LEADER 05803nam 22006855 450 001 9910473455503321 005 20230220210428.0 010 $a3-030-72013-6 024 7 $a10.1007/978-3-030-72013-1 035 $a(CKB)4100000011807336 035 $a(MiAaPQ)EBC6524978 035 $a(Au-PeEL)EBL6524978 035 $a(OCoLC)1246184909 035 $a(oapen)https://directory.doabooks.org/handle/20.500.12854/67936 035 $a(DE-He213)978-3-030-72013-1 035 $a(PPN)254719171 035 $a(EXLCZ)994100000011807336 100 $a20210322d2021 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aTools and Algorithms for the Construction and Analysis of Systems $e27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 ? April 1, 2021, Proceedings, Part II /$fedited by Jan Friso Groote, Kim Guldstrand Larsen 205 $a1st ed. 2021. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2021. 215 $a1 online resource (476 pages) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12652 311 $a3-030-72012-8 327 $aVerification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- Bridging Arrays and ADTs in Recursive Proofs -- A Two-Phase Approach for Conditional Floating-Point Verification -- Symbolic Coloured SCC Decomposition -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- Syntax-Guided Quantifier Instantiation -- Making Theory Reasoning Simpler -- Deductive Stability Proofs for Ordinary Differential Equations -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- cake lpr: Verified Propagation Redundancy Checking in CakeML -- Deductive Veri cation of Floating-Point Java Programs in KeY -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- SyReNN: A Tool for Analyzing Deep Neural Networks -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- AMulet 2.0 for Verifying Multiplier Circuits -- RTLola on Board: Testing Real Driving Emissions on your Phone -- Replicating Restart with Prolonged Retrials: An Experimental Report -- A Web Interface for Petri Nets with Transits and Petri Games -- Momba: JANI Meets Python -- SV-Comp Tool Competition Papers -- Software Veri cation: 10th Comparative Evaluation (SV-COMP 2021) -- CPALockator: Thread-Modular Approach with Projections (Competition Contribution) -- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution) -- Gazer-Theta: LLVM-based Veri er Portfolio with BMC/CEGAR (Competition Contribution) -- Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution) -- Towards String Support in JayHorn (Competition Contribution) -- JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) -- Symbiotic 8: Beyond Symbolic Execution (Competition Contribution) -- VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). 330 $aThis open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 ? April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12652 606 $aComputer science 606 $aComputer engineering 606 $aComputer networks 606 $aMicroprogramming 606 $aSoftware engineering 606 $aTheory of Computation 606 $aComputer Engineering and Networks 606 $aControl Structures and Microprogramming 606 $aSoftware Engineering 615 0$aComputer science. 615 0$aComputer engineering. 615 0$aComputer networks. 615 0$aMicroprogramming. 615 0$aSoftware engineering. 615 14$aTheory of Computation. 615 24$aComputer Engineering and Networks. 615 24$aControl Structures and Microprogramming. 615 24$aSoftware Engineering. 676 $a004.0151 700 $aGroote$b Jan Friso$0846119 701 $aLarsen$b Kim Guldstrand$0846120 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910473455503321 996 $aTools and Algorithms for the Construction and Analysis of Systems$91890034 997 $aUNINA