001463059 000__ 06378cam\a22006617i\4500 001463059 001__ 1463059 001463059 003__ OCoLC 001463059 005__ 20230601003303.0 001463059 006__ m\\\\\o\\d\\\\\\\\ 001463059 007__ cr\un\nnnunnun 001463059 008__ 230424s2023\\\\sz\a\\\\o\\\\\101\0\eng\d 001463059 020__ $$a9783031308239$$q(electronic bk.) 001463059 020__ $$a3031308239$$q(electronic bk.) 001463059 020__ $$z9783031308222 001463059 0247_ $$a10.1007/978-3-031-30823-9$$2doi 001463059 035__ $$aSP(OCoLC)1377209777 001463059 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dYDX 001463059 049__ $$aISEA 001463059 050_4 $$aQA76.9.S88$$bT33 2023 001463059 08204 $$a004.2/1$$223/eng/20230424 001463059 1112_ $$aTACAS (Conference)$$n(29th :$$d2023 :$$cParis, France) 001463059 24510 $$aTools and algorithms for the construction and analysis of systems :$$b29th International Conference, TACAS 2023, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings.$$nPart I /$$cSriram Sankaranarayanan, Natasha Sharygina, editors. 001463059 2463_ $$aTACAS 2023 001463059 264_1 $$aCham, Switzerland :$$bSpringer,$$c[2023] 001463059 300__ $$a1 online resource (xxiii, 708 pages) :$$billustrations (some color). 001463059 336__ $$atext$$btxt$$2rdacontent 001463059 337__ $$acomputer$$bc$$2rdamedia 001463059 338__ $$aonline resource$$bcr$$2rdacarrier 001463059 4901_ $$aLecture Notes in Computer Science,$$x1611-3349 ;$$v13993 001463059 4901_ $$aAdvanced research in computing and software science 001463059 500__ $$aIncludes author index. 001463059 5050_ $$aInvited Talk.-A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems -- Model Checking -- Bounded Model Checking for Asynchronous Hyperproperties -- Model Checking Linear Dynamical Systems under Floating-point Rounding -- Efficient Loop Conditions for Bounded Model Checking Hyperproperties -- Reconciling Preemption Bounding with DPOR -- Optimal Stateless Model Checking for Causal Consistency -- Symbolic Model Checking for TLA+ Made Faster -- AutoHyper: Explicit-State Model Checking for HyperLTL -- Machine Learning/Neural Networks -- Feature Necessity & Relevancy in ML Classifier Explanations -- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks -- OccRob: Effcient SMT-Based Occlusion Robustness Verification of Deep Neural Networks -- Neural Network-Guided Synthesis of Recursive List Functions -- Automata -- Modular Mix-and-Match Complementation of Buechi automata -- Validating Streaming JSON Documents With Learned VPAs -- Antichains Algorithms for the Inclusion Problem Between -VPL -- Stack-Aware Hyperproperties -- Proofs -- Propositional Proof Skeletons -- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers -- Carcara: An effcient proof checker and elaborator for SMT proofs in the Alethe format -- Constraint Solving/Blockchain -- The Packing Chromatic Number of the Infinite Square Grid is 15 -- Active Learning for SAT Solver Benchmarking -- ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving -- Inferring Needless Write Memory Accesses on Ethereum Bytecode -- Markov Chains/Stochastic Control -- A Practitioner's Guide to MDP Model Checking Algorithms -- Correct Approximation of Stationary Distributions -- Robust Almost-Sure Reachability in Multi-Environment MDPs -- Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning -- Verification -- A Formal CHERI-C Semantics for Verification -- Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm -- Parameterized Verification under TSO with Data Types -- Verifying Learning-Based Robotic Navigation Systems: A Case Study -- Make flows small again: revisiting the flow framework -- ALASCA: Reasoning in Quantified Linear Arithmetic -- A Matrix-Based Approach to Parity Games -- A GPU Tree Database for Many-Core Explicit State Space Exploration. 001463059 5060_ $$aOpen access.$$5GW5XE 001463059 520__ $$aThis open access book constitutes the proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, during April 22-27, 2023, in Paris, France. The 56 full papers and 6 short tool demonstration papers presented in this volume were carefully reviewed and selected from 169 submissions. The proceedings also contain 1 invited talk in full paper length, 13 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report. TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility, and efficiency of tools and algorithms for building computer-controlled systems. 001463059 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed April 24, 2023). 001463059 650_0 $$aSystem design$$vCongresses. 001463059 650_0 $$aComputer software$$xVerification$$vCongresses. 001463059 650_0 $$aSystem analysis$$vCongresses. 001463059 655_0 $$aElectronic books. 001463059 7001_ $$aSankaranarayanan, Sriram,$$eeditor.$$1https://orcid.org/0000-0001-7315-4340 001463059 7001_ $$aSharygina, Natasha,$$eeditor.$$1https://orcid.org/0000-0002-8872-4913 001463059 7112_ $$aETAPS (Conference)$$n(26th :$$d2023 :$$cParis, France) 001463059 830_0 $$aLecture notes in computer science ;$$v13993.$$x1611-3349 001463059 830_0 $$aLecture notes in computer science.$$pAdvanced research in computing and software science. 001463059 852__ $$bebk 001463059 85640 $$3Springer Nature$$uhttps://link.springer.com/10.1007/978-3-031-30823-9$$zOnline Access$$91397441.2 001463059 909CO $$ooai:library.usi.edu:1463059$$pGLOBAL_SET 001463059 980__ $$aBIB 001463059 980__ $$aEBOOK 001463059 982__ $$aEbook 001463059 983__ $$aOnline 001463059 994__ $$a92$$bISE