001463060 000__ 07352cam\a22006617i\4500 001463060 001__ 1463060 001463060 003__ OCoLC 001463060 005__ 20230601003303.0 001463060 006__ m\\\\\o\\d\\\\\\\\ 001463060 007__ cr\un\nnnunnun 001463060 008__ 230424s2023\\\\sz\a\\\\o\\\\\001\0\eng\d 001463060 020__ $$a9783031308208$$q(electronic bk.) 001463060 020__ $$a3031308204$$q(electronic bk.) 001463060 020__ $$z9783031308192$$q(print) 001463060 0247_ $$a10.1007/978-3-031-30820-8$$2doi 001463060 035__ $$aSP(OCoLC)1377209783 001463060 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dYDX 001463060 049__ $$aISEA 001463060 050_4 $$aQA76.9.S88$$bT33 2023 001463060 08204 $$a004.2/1$$223/eng/20230424 001463060 1112_ $$aTACAS (Conference)$$n(29th :$$d2023 :$$cParis, France) 001463060 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 II /$$cSriram Sankaranarayanan, Natasha Sharygina, editors. 001463060 2463_ $$aTACAS 2023 001463060 264_1 $$aCham :$$bSpringer,$$c[2023] 001463060 300__ $$a1 online resource (xxiv, 604 pages) :$$billustrations (some color). 001463060 336__ $$atext$$btxt$$2rdacontent 001463060 337__ $$acomputer$$bc$$2rdamedia 001463060 338__ $$aonline resource$$bcr$$2rdacarrier 001463060 4901_ $$aLecture notes in computer science,$$x1611-3349 ;$$v13994 001463060 4901_ $$aAdvanced research in computing and software science 001463060 500__ $$aIncludes author index. 001463060 5050_ $$aTool Demos -- EVA: a Tool for the Compositional Verification of AUTOSAR Models -- WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification -- Multiparty Session Typing in Java, Deductively -- PyLTA: A Verification Tool for Parameterized Distributed Algorithms -- FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format -- Eclipse ESCETâ„¢: The Eclipse Supervisory Control Engineering Toolkit -- Combinatorial Optimization/Theorem Proving -- New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization -- Verified reductions for optimization -- Specifying and Verifying Higher-order Rust Iterators -- Extending a High-Performance Prover to Higher-Order Logic -- Tools (Regular Papers) -- The WhyRel Prototype for Relational Verification of Pointer Programs -- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter -- CoPTIC: Constraint Programming Translated Into C -- Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability -- Synthesis -- Computing Adequately Permissive Assumptions for Synthesis -- Verification-guided Programmatic Controller Synthesis -- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications -- Lockstep Composition for Unbalanced Loops -- Synthesis of Distributed Agreement-Based Systems with Effciently Decidable Verification -- LTL Reactive Synthesis with a Few Hints -- Timed Automata Verification and Synthesis via Finite Automata Learning -- Graphs/Probabilistic Systems -- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition -- Transforming quantified Boolean formulas using biclique covers -- Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration -- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants -- Runtime Monitoring/Program Analysis -- Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote -- Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis -- Explainable Online Monitoring of Metric Temporal Logic -- 12th Competition on Software Verification -- SV-COMP 2023 -- Competition on Software Verification and Witness Validation: SV-COMP 2023 -- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution) -- 2LS: Arrays and Loop Unwinding (Competition Contribution) -- Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution) -- EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution) -- Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution) -- Java Ranger: Supporting String and Array Operations (Competition Contribution) -- Korn-Software Verification with Horn Clauses (Competition Contribution) -- Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution) -- PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution) -- Ultimate Automizer and the CommuHash Normal Form (Competition Contribution) -- Ultimate Taipan and Race Detection in Ultimate (Competition Contribution) -- VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution) -- VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution). 001463060 5060_ $$aOpen access.$$5GW5XE 001463060 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. 001463060 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed April 24, 2023). 001463060 650_0 $$aSystem design$$vCongresses. 001463060 650_0 $$aComputer software$$xVerification$$vCongresses. 001463060 650_0 $$aSystem analysis$$vCongresses. 001463060 655_0 $$aElectronic books. 001463060 7001_ $$aSankaranarayanan, Sriram,$$eeditor.$$1https://orcid.org/0000-0001-7315-4340 001463060 7001_ $$aSharygina, Natasha,$$eeditor.$$1https://orcid.org/0000-0002-8872-4913 001463060 7112_ $$aETAPS (Conference)$$n(26th :$$d2023 :$$cParis, France) 001463060 830_0 $$aLecture notes in computer science ;$$v13994.$$x1611-3349 001463060 830_0 $$aLecture notes in computer science.$$pAdvanced research in computing and software science. 001463060 852__ $$bebk 001463060 85640 $$3Springer Nature$$uhttps://link.springer.com/10.1007/978-3-031-30820-8$$zOnline Access$$91397441.2 001463060 909CO $$ooai:library.usi.edu:1463060$$pGLOBAL_SET 001463060 980__ $$aBIB 001463060 980__ $$aEBOOK 001463060 982__ $$aEbook 001463060 983__ $$aOnline 001463060 994__ $$a92$$bISE