LEADER 05348nam 22005175 450 001 9910717415303321 005 20241120180423.0 010 $a3-031-30823-9 024 7 $a10.1007/978-3-031-30823-9 035 $a(CKB)5720000000183523 035 $a(NjHacI)995720000000183523 035 $a(MiAaPQ)EBC7241009 035 $a(Au-PeEL)EBL7241009 035 $a(DE-He213)978-3-031-30823-9 035 $a(PPN)269655352 035 $a(OCoLC)1377209777 035 $a(EXLCZ)995720000000183523 100 $a20230421d2023 u| 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aTools and Algorithms for the Construction and Analysis of Systems $e29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22?27, 2023, Proceedings, Part I /$fedited by Sriram Sankaranarayanan, Natasha Sharygina 205 $a1st ed. 2023. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2023. 215 $a1 online resource (xxiii, 708 pages) $cillustrations (some color) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v13993 311 $a3-031-30822-0 320 $aIncludes bibliographical references and index. 327 $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. 330 $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. 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v13993 606 $aComputer science 606 $aTheory of Computation 615 0$aComputer science. 615 14$aTheory of Computation. 676 $a005.1 702 $aSankaranarayanan$b Sriram 702 $aSharygina$b Natasha 801 0$bNjHacI 801 1$bNjHacl 906 $aBOOK 912 $a9910717415303321 996 $aTools and Algorithms for the Construction and Analysis of Systems$9772021 997 $aUNINA