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

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

Show other versions (1)
Saved in:
Bibliographic Details
Superior document:Lecture Notes in Computer Science Series ; v.12760
:
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
Online Access:
Physical Description:1 online resource (955 pages)
Tags: Add Tag
No Tags, Be the first to tag this record!
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.

Similar Items