Computer Aided Verification : : 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I.

• Superior document: Lecture Notes in Computer Science Series ; v.13371
• Author: Shoham, Sharon.
• TeilnehmendeR: Vizel, Yakir.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2022.; ©2022.
• Year of Publication: 2022
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (563 pages)

Table of Contents

Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Papers -- A Billion SMT Queries a Day (Invited Paper) -- 1 Introduction -- 2 Eliminate Writing Specifications -- 2.1 Generating Possible Specifications (Findings) -- 3 Domain-Specific Abstractions -- 4 SMT Solving at Cloud Scale -- 4.1 Monotonicity in Runtimes Across Solver Versions -- 4.2 Stability of the Solvers -- 4.3 Concluding Remarks -- References -- Program Verification with Constrained Horn Clauses (Invited Paper) -- 1 Introduction -- 2 Logic of Constrained Horn Clauses -- 3 Solving CHC Modulo Theories -- References -- Formal Methods for Probabilistic Programs -- Data-Driven Invariant Learning for Probabilistic Programs -- 1 Introduction -- 2 Preliminaries -- 3 Algorithm Overview -- 4 Learning Exact Invariants -- 4.1 Generate Features (getFeatures) -- 4.2 Sample Initial States (sampleStates) -- 4.3 Sample Training Data (sampleTraces) -- 4.4 Learning a Model Tree (learnInv) -- 4.5 Extracting Expectations from Models (extractInv) -- 4.6 Verify Extracted Expectations (verifyInv) -- 5 Learning Sub-invariants -- 5.1 Sample Training Data (sampleTraces) -- 5.2 Learning a Neural Model Tree (learnInv) -- 5.3 Verify Extracted Expectations (verifyInv) -- 6 Evaluations -- 6.1 R1: Evaluation of the Exact Invariant Method -- 6.2 R2: Evaluation of the Sub-invariant Method -- 7 Related Work -- References -- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 4 A Sound and Complete Characterization of SIs -- 5 Stochastic Invariants for LBPT -- 6 Automated Template-Based Synthesis Algorithm -- 7 Experimental Results -- 8 Related Works -- 9 Conclusion -- References -- Does a Program Yield the Right Distribution? -- 1 Introduction -- 2 Generating Functions.

2.1 The Ring of Formal Power Series -- 2.2 Probability Generating Functions -- 3 ReDiP: A Probabilistic Programming Language -- 3.1 Program States and Variables -- 3.2 Syntax of ReDiP -- 3.3 The Statement x += iid(D, y) -- 4 Interpreting ReDiP with PGF -- 4.1 A Domain for Distribution Transformation -- 4.2 From Programs to PGF Transformers -- 4.3 Probabilistic Termination -- 5 Reasoning About Loops -- 5.1 Fixed Point Induction -- 5.2 Deciding Equivalence of Loop-free Programs -- 6 Case Studies -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Abstraction-Refinement for Hierarchical Probabilistic Models -- 1 Introduction -- 2 Overview -- 3 Formal Problem Statement -- 3.1 Background -- 3.2 Hierarchical MDPs -- 3.3 Optimal Local Subpolicies and Beyond -- 4 Solving hMDPs with Abstraction-Refinement -- 4.1 The Macro-MDP Formulation -- 4.2 The Uncertain Macro-MDP Formulation -- 4.3 Set-Based SubMDP Analysis -- 4.4 Templates for Set-Based subMDP Analysis -- 5 Implementing the Abstraction-Refinement Loop -- 6 Experiments -- 7 Related Work -- 8 Conclusion -- References -- Formal Methods for Neural Networks -- Shared Certificates for Neural Network Verification -- 1 Introduction -- 2 Background -- 3 Proof Sharing with Templates -- 3.1 Motivation: Proof Subsumption -- 3.2 Proof Sharing with Templates -- 4 Efficient Verification via Proof Sharing -- 4.1 Choice of Abstract Domain -- 4.2 Template Generation -- 4.3 Robustness to Adversarial Patches -- 4.4 Geometric Robustness -- 4.5 Requirements for Proof Sharing -- 5 Experimental Evaluation -- 5.1 Experimental Setup -- 5.2 Robustness Against Adversarial Patches -- 5.3 Robustness Against Geometric Perturbations -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion -- References -- Example Guided Synthesis of Linear Approximations for Neural Network Verification -- 1 Introduction.

2 Preliminaries -- 2.1 Neural Networks -- 2.2 Existing Neural Network Verification Techniques and Limitations -- 3 Problem Statement and Challenges -- 3.1 The Synthesis Problem -- 3.2 Challenges and Our Solution -- 4 Our Approach -- 4.1 Partitioning the Input Interval Space (Ix) -- 4.2 Learning the Function g(l, u) -- 4.3 Ensuring Soundness of the Linear Approximations -- 4.4 Efficient Lookup of the Linear Bounds -- 5 Evaluation -- 5.1 Benchmarks -- 5.2 Experimental Results -- 6 Related Work -- 7 Conclusions -- References -- Verifying Neural Networks Against Backdoor Attacks -- 1 Introduction -- 2 Problem Definition -- 3 Verifying Backdoor Absence -- 3.1 Overall Algorithm -- 3.2 Verifying Backdoor Absence Against a Set of Images -- 3.3 Abstract Interpretation -- 3.4 Generating Backdoor Triggers -- 3.5 Correctness and Complexity -- 3.6 Discussion -- 4 Implementation and Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning -- 1 Introduction -- 2 Deep Reinforcement Learning (DRL) -- 3 Model Checking of DRL Systems -- 3.1 The Model Checking Problem -- 3.2 Challenges in Model Checking DRL Systems -- 4 The CEGAR-Driven DRL Approach -- 4.1 The Framework -- 4.2 Training on Abstract States -- 4.3 Model Checking Trained DRL Systems -- 4.4 Counterexample-Guided Refinement -- 5 Implementation and Evaluation -- 5.1 Implementation -- 5.2 Benchmarks and Experimental Settings -- 5.3 Reliability and Verifiability Comparison -- 5.4 Performance Comparison -- 6 Related Work -- 7 Discussion and Conclusion -- References -- Neural Network Robustness as a Verification Property: A Principled Case Study -- 1 Introduction -- 2 Existing Training Techniques and Definitions of Robustness -- 3 Robustness in Evaluation, Attack and Verification.

4 Relative Comparison of Definitions of Robustness -- 4.1 Standard and Lipschitz Robustness -- 4.2 (Strong) Classification Robustness -- 4.3 Standard vs Classification Robustness -- 5 Other Properties of Robustness Definitions -- 6 Conclusions -- References -- Software Verification and Model Checking -- The Lattice-Theoretic Essence of Property Directed Reachability Analysis*-12pt -- 1 Introduction -- 2 Fixed-points in Complete Lattices -- 3 Lattice-Theoretic Reconstruction of PDR -- 3.1 Positive LT-PDR: Sequential Positive Witnesses -- 3.2 Negative PDR: Sequential Negative Witnesses -- 3.3 LT-PDR: Integrating Positive and Negative -- 4 Structural Theory of PDR by Category Theory -- 4.1 Categorical Modeling of Dynamics and Predicate Transformers -- 4.2 Structural Theory of PDR from Transition Systems -- 5 Known and New PDR Algorithms as Instances -- 5.1 LT-PDRs for Kripke Structures: PDRF-Krand PDRIB-Kr -- 5.2 LT-PDR for MDPs: PDRIB-MDP -- 5.3 LT-PDR for Markov Reward Models: PDRMRM -- 6 Implementation and Evaluation -- 7 Conclusions and Future Work -- References -- Affine Loop Invariant Generation via Matrix Algebra -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 Affine Invariants via Farkas' Lemma -- 4 Single-Branch Affine Loops with Deterministic Updates -- 4.1 Derived Constraints from the Farkas Tables -- 4.2 Loops with Tautological Guard -- 4.3 Loops with Guard: Single-Constraint Case -- 4.4 Loops with Guard: Multi-constraint Case -- 5 Generalizations -- 5.1 Affine Loops with Non-deterministic Updates -- 5.2 An Extension to Bidirectional Affine Invariants -- 5.3 Other Possible Generalizations -- 6 Approximation of Eigenvectors through Continuity -- 7 Experimental Results -- References -- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes -- 1 Introduction.

2 Safety Verification Using Learning of Invariants -- 2.1 Linear Constraints and Safety Verification -- 2.2 The ICE Learning Framework -- 2.3 ICE-DT: Invariant Learning Using Decision Trees -- 3 Linear Formulas as Abstract Objects -- 4 Generating Attributes from Sample Separators -- 4.1 Abstract Sample Separators -- 4.2 Computing a Join-Maximal Abstract Separator -- 4.3 Integrating Separator Computation in ICE-DT -- 4.4 Computing Separators Incrementally -- 5 Experiments -- 6 Conclusion -- References -- Proof-Guided Underapproximation Widening for Bounded Model Checking -- 1 Introduction -- 2 Background -- 2.1 Language Model -- 2.2 VC Generation for a Procedure -- 2.3 Static Versus Dynamic Inlining -- 2.4 Verification with Stratified Inlining -- 2.5 Overapproximation Refinement Guided Stratified Inlining -- 3 Overview -- 3.1 Underapproximation Widening -- 4 Algorithms -- 4.1 Underapproximation Widening Guided Stratified Inlining (UnderWidenSI) -- 4.2 Portfolio Technique -- 5 Experimental Results -- 5.1 Corral Versus Legion -- 5.2 Performance of Legion+ -- 6 Related Work -- 7 Conclusion -- References -- SolCMC: Solidity Compiler's Model Checker -- 1 Introduction -- 2 Solidity Model Checking -- 2.1 The CHC Verification Engine -- 2.2 Horn Encoding -- 3 User Features -- 4 Real World Experiments -- 4.1 CHC Solver Options -- 4.2 Deposit Contract -- 4.3 ERC777 -- 4.4 Discussion -- 5 Conclusions and Future Work -- References -- Hyperproperties and Security -- Software Verification of Hyperproperties Beyond k-Safety -- 1 Introduction -- 1.1 Verification Beyond k-Safety -- 1.2 Contributions and Structure -- 2 Overview: Reductions and Quantification as a Game -- 2.1 Reductions as a Game -- 2.2 Beyond k-Safety: Quantification as a Game -- 3 Preliminaries -- 4 Observation-Based HyperLTL -- 5 Reductions as a Game -- 6 Verification Beyond k-Safety.

6.1 Existential Trace Quantification as a Game.