Computer Aided Verification : : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II.

• Superior document: Lecture Notes in Computer Science Series ; v.12760
• Author: Silva, Alexandra.
• TeilnehmendeR: Leino, K. Rustan M.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2021.; ©2021.
• Year of Publication: 2021
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (955 pages)

Table of Contents

Intro -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Complexity and Termination -- Learning Probabilistic Termination Proofs -- 1 Introduction -- 2 Termination Analysis of Probabilistic Programs -- 3 Training Neural Ranking Supermartingales -- 4 Verifying Ranking Supermartingales by SMT Solving -- 4.1 From Programs to Symbolic Store Trees -- 4.2 Marginalisation -- 5 Case Studies -- 5.1 Non-linear Program Expressions and NRSMs -- 5.2 Multivariate and Hierarchical Distributions -- 5.3 State-Dependent Distributions and Non-Linear Expectations -- 5.4 Undefined Moments -- 5.5 Rare Transitions -- 6 Experimental Results -- 7 Conclusion -- References -- Ghost Signals: Verifying Termination of Busy Waiting -- 1 Introduction -- 2 A Guide on Verifying Termination of Busy Waiting -- 2.1 Simplest Setting: Thread-Safe Physical Signals -- 2.2 Non-Thread-Safe Physical Signals -- 2.3 Arbitrary Data Structures -- 2.4 Signal Erasure -- 3 A Realistic Example -- 4 Specifying Busy-Waiting Concurrent Objects -- 5 Tool Support -- 6 Integrating Higher-Order Features -- 7 Related and Future Work -- 8 Conclusion -- References -- Reflections on Termination of Linear Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 3 Linear Abstractions of Transition Formulas -- 3.1 Affine Abstractions of Transition Formulas -- 3.2 Reflections via the Dual Space -- 3.3 Determinization -- 3.4 Rational-Spectrum Reflections of DATS -- 4 Asymptotic Analysis of Linear Dynamical Systems -- 5 A Conditional Termination Analysis for Programs -- 6 Evaluation -- 7 Related Work -- References -- Decision Tree Learning in CEGIS-Based Termination Analysis -- 1 Introduction -- 2 Preview by Examples -- 2.1 Termination Verification by CEGIS -- 2.2 Handling Cycles in Decision Tree Learning -- 3 (Non-)Termination Verification as Constraint Solving.

4 CounterExample-Guided Inductive Synthesis (CEGIS) -- 5 Ranking Function Synthesis -- 5.1 Basic Definitions -- 5.2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case -- 5.3 Segmentation and (Explicit and Implicit) Cycles: Multi-Dimensional Lexicographic Case -- 5.4 Our Decision Tree Learning Algorithm -- 5.5 Improvement by Degenerating Negative Values -- 6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusions and Future Work -- References -- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures -- 1 Introduction -- 2 Step by Step to an Automated Analysis of Splaying -- 3 Technical Foundation -- 4 The Road to Automation, Continued -- 4.1 Type Checking -- 4.2 Type Inference -- 5 Implementation -- 5.1 The Three Phases of ATLAS -- 5.2 Details on the Generation of the Constraint System -- 5.3 Optimisation -- 6 Evaluation -- 6.1 Automated Analysis of Splaying et al. -- 6.2 Experimental Results -- 7 Conclusion -- References -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 3.1 Term Rewriting Systems -- 3.2 Compact Representation Using Equality Graphs -- 4 Theory Synthesis -- 4.1 Term Generation -- 4.2 Conjecture Inference and Screening -- 4.3 Induction Prover -- 4.4 Looping Back -- 5 Evaluation -- 5.1 Evaluating Theory Exploration Quality -- 5.2 Efficacy to Automated Proving -- 6 Related Work -- 7 Conclusion -- References -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- 1 Introduction -- 2 Methodology Overview -- 3 Preliminaries -- 4 Bit-Vector Theory -- 5 Theory for SMT QF_BV Queries -- 5.1 Syntax of SMT QF_BV Queries -- 5.2 Semantics of SMT QF_BV Queries -- 5.3 Derived QF_BV Operations and Predicates -- 6 Certified Bit Blasting -- 7 A Certified SMT QF_BV Solver -- 8 Experiments.

8.1 SMT QF_BV Competition -- 8.2 Linear Field Arithmetic in Cryptography -- 9 Conclusion -- References -- Porous Invariants -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 R Invariants: R-linear and R-semi-linear -- 4 Strongest Z-linear Invariants -- 4.1 Extensions of Z-linear Sets Without Strongest Invariants -- 4.2 Z-linear Targets -- 5 N-Semi-linear Invariants -- 5.1 Existence of Sufficient (but Non-minimal) N-semi-linear Invariants for Point Reachability in Deterministic LDS -- 5.2 Undecidability of N-semi-linear Invariants for Nondeterministic LDS -- 5.3 Nondeterministic One-Dimensional Affine Updates -- 6 The POROUS Tool -- 7 Conclusions and Open Directions -- References -- JavaSMT 3: Interacting with SMT Solvers in Java -- 1 Introduction -- 2 JavaSMT's Architecture and Solver Integration -- 3 New Contributions in JavaSMT 3 -- 4 Evaluation -- 5 Conclusion -- References -- Efficient SMT-Based Analysis of Failure Propagation -- 1 Introduction -- 2 Preliminaries -- 3 Propagation Graphs over FDSs -- 4 From Sequential to Combinational -- 5 Enumeration of FDS-Minimal Cut Sets -- 5.1 Algorithm for Boolean FDSs -- 5.2 Extension to Arbitrary FDSs -- 6 Related Work -- 6.1 Detailed Comparison with Finite Degradation Models -- 7 Experimental Evaluation -- 8 Conclusions and Further Work -- References -- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends -- 1 Introduction -- 2 Detecting Failure-Inducing Inputs -- 3 Simplification Rules and Staged Simplification -- 4 Parsing and Input Representation -- 5 Delta Debugging Strategies -- 6 Experimental Evaluation -- 7 Conclusion -- References -- Learning Union of Integer Hypercubes with Queries -- 1 Introduction -- 2 Preliminaries -- 3 Minimally Adequate Teacher -- 3.1 Corner Oracle -- 3.2 Overshooting Algorithm -- 3.3 Repetition-Free Complexity -- 4 Extensions.

4.1 Maximal Cube Oracle -- 4.2 Maximal Cube Algorithm -- 4.3 Extension to the Infinite Case -- 4.4 Complexity -- 5 Applications and Experiments -- 5.1 Application to Monadic Decomposition -- 5.2 Experiments -- 5.3 Benchmark Suite -- 5.4 Results -- 6 Conclusion and Future Work -- References -- Interpolation and Model Checking for Nonlinear Arithmetic -- 1 Introduction -- 2 Background -- 3 SMT Modulo Models and Interpolation -- 3.1 Interpolation -- 3.2 SMT Modulo Models with MCSAT -- 4 Nonlinear Arithmetic -- 5 Evaluation -- 5.1 Related Work -- 6 Conclusion and Future Work -- References -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- 1 Introduction -- 2 Preliminaries -- 2.1 Basic Definitions -- 2.2 Theoretical Landscape -- 3 Length-Aware Regular Expression Algorithm -- 3.1 High-Level Algorithm -- 4 Length-Aware and Prefix/Suffix Heuristics in Z3str3RE -- 4.1 Computing Length Information from Regexes -- 4.2 Optimizing Automata Operations via Length Information -- 4.3 Leveraging Length Information to Optimize Search -- 4.4 Prefix/Suffix Over-Approximation Heuristic -- 5 Empirical Results -- 5.1 Empirical Setup and Solvers Used -- 5.2 Benchmarks -- 5.3 Comparison and Scoring Methods -- 5.4 Analysis of Empirical Results -- 5.5 Detailed Experimental Results -- 5.6 Analysis of Individual Heuristics and Results -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Counting Minimal Unsatisfiable Subsets -- 1 Introduction -- 2 Preliminaries and Problem Definition -- 3 Related Work -- 4 MUS Counting via a Projected Model Counter -- 4.1 Basic MUS Counting Idea -- 4.2 W1 - the Base Wrapper and Its Reminder -- 4.3 W2 - the Intersection of MUSes -- 4.4 W3 - The Union of MUSes -- 4.5 W4 - Minimum MUS Cardinality -- 4.6 W5 - Maximum MUS Cardinality -- 4.7 W6 - Component Partitioning.

4.8 W7 - Minimal Hitting Set Duality -- 4.9 W8 - Literal Negation Cover -- 4.10 W9 - Non-extendable Evidence Models -- 4.11 W10 - Enforced Evidence Models -- 4.12 Combining Wrappers and Their Remainders -- 5 Experimental Evaluation -- 5.1 Solved Benchmarks -- 5.2 Scalability W.r.t the MUS Count -- 5.3 Accuracy of Wrappers -- 6 Future Possible Applications of Wrappers and Remainders -- 7 Conclusion and Future Work -- References -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- 1 Introduction -- 2 The Cervino Language -- 2.1 Sorts, Relations and Axioms -- 2.2 Events -- 2.3 Commands -- 3 Background on FOLTL -- 3.1 Syntax and Semantics of FOLTL -- 3.2 Bounded Domain Property -- 3.3 Semantics of Cervino -- 4 Basic Transformations -- 4.1 Transforming Equality -- 4.2 Restricted Skolemization -- 4.3 Instantiation -- 4.4 Addressing Transitive Closure and the Between Relation -- 4.5 Geneva Transformation -- 5 TEA: Transforming Existential Quantifiers -- 6 TFC: Transforming Frame Conditions -- 7 TTC: Transforming Reflexive-Transitive Closure -- 8 Evaluation -- 9 Related Work -- 10 Conclusion -- References -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- 1 Introduction -- 2 Circuits -- 3 Model Checking -- 4 Certification -- 5 Implementation -- 6 Experiments -- 7 Conclusion -- References -- Model-Checking Structured Context-Free Languages -- 1 Introduction -- 2 Operator Precedence Languages -- 2.1 Operator Precedence Omega-Languages -- 2.2 Modeling Programs with OPA -- 3 POTL: Syntax and Semantics -- 3.1 Expressiveness of POTL -- 4 Model Checking -- 4.1 Model Checking for Omega-Words -- 4.2 Complexity -- 5 Experimental Evaluation -- 6 Conclusions -- References -- Model Checking -Regular Properties with Decoupled Search -- 1 Introduction -- 2 Büchi Automata, Composition and Verification.

3 The Decoupled State Space for Composed NBAs.