Verification, Model Checking, and Abstract Interpretation : 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16–17, 2023, Proceedings

This book constitutes the proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023, which took place in Boston, USA, in January 2023. The 17 full papers presented in this book were carefully reviewed and selected from 34 submissions. The contributions deal with program verification, model checking, abstract interpretation, program synthesis, static analysis, type systems, deductive methods, decision procedures, theorem proving, program certification, debugging techniques, program transformation, optimization, and hybrid and cyber-physical systems. Preface Organization Contents Distributing and Parallelizing Non-canonical Loops 1 Original Approaches to Automatic Parallelization 1.1 The Challenge of Unknown Iteration Space 1.2 Motivations for Correct, Universal and Automatic Parallelization 1.3 Our Technique: Properties, Benefits and Limitations 1.4 Contributions: From Theory to Benchmarks 2 Background: Language and Dependency Analysis 2.1 A Simple While Imperative Language with Parallel Capacities 2.2 Data-Flow Graphs for Loop Dependency Analysis 2.3 Constructing Data-Flow Graphs 3 Loop Fission Algorithm 3.1 Algorithm, Presentation and Intuition 3.2 Correctness of the Algorithm 4 Limitations of Existing Alternative Approaches 4.1 Comparing Dependency Analyses 4.2 Assessment of Existing Automated Loop Transformation and Parallelization Tools 5 Evaluation 5.1 Benchmarks 5.2 Results 6 Conclusion References SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study 1 Introduction 2 Spiking Neural Networks 2.1 Discretized Simulation Time 2.2 Spike Trains and Encoding from Feature Inputs 2.3 Leaky Integrate and Fire (LIFR) Neuron 3 SMT Encoding of SNN 4 The Proposed Framework 4.1 Encoding of Input and Output Properties 4.2 Overall Verification Framework 4.3 Verifying Adversarial Robustness of SNNs 5 Implementation and Results 5.1 Verification Results on the Iris Dataset 5.2 Adversarial Robustness for Iris and MNIST 6 Related Work 7 Conclusion and Future Directions References StaticPersist: Compiler Support for PMEM Programming 1 Introduction 2 Motivating Example 3 Algorithm 3.1 Points-To Algorithm Based on Allocation-Site 3.2 Allocation-Stack with Bounded Depth 3.3 Inter-procedural DFA Specification 4 Evaluation 5 Related Work 6 Conclusions and Future Work References Symbolic Abstract Heaps for Polymorphic Information-Flow Guard Inference 1 Introduction 2 Preliminaries 3 Symbolic Abstract Heap Domains 3.1 Families of Heap-Related Relations 3.2 Symbolic Abstract Heap Domain 3.3 Instances of Symbolic Abstract Heap Domains 4 Secure Heap Abstraction 5 Inferring Polymorphic Information-Flow Guards 5.1 Security Semantics 5.2 Guard Inference Procedure 5.3 Soundness 6 Implementation and Evaluation 7 Discussions References Satisfiability Modulo Custom Theories in Z3 1 Introduction 2 Motivating Example 3 User-Propagators in Z3 3.1 Workflow for User-Propagators 3.2 Supported Callbacks 4 User-Propagators for Memory Reasoning in alive2 5 Using User-Propagators 6 Related Work 7 Conclusions and Future Work References Bayesian Parameter Estimation with Guarantees via Interval Analysis and Simulation 1 Introduction 2 Problem Statement 3 Interval Arithmetic, Discretized odeS, Neural Networks 3.1 Interval Arithmetic, Coverings, Set Inversion 3.2 Discretized odeS and Neural Networks 4 The Core Algorithm A 5 Confidence Intervals for Posterior Moments 6 Optimal Allocation of Computational Resources 7 Experiments 7.1 Discretized odeS 7.2 Feature Relevance in Neural Network Classifiers 8 Conclusion References A Pragmatic Approach to Stateful Partial Order Reduction 1 Introduction 2 Preliminaries 2.1 Partial Order Reduction 3 Eager Source Set POR (DE-S-POR) 3.1 Safe Set POR (S-POR) 3.2 Full Algorithm 4 Lazy Source Set POR (DL-S-POR) 5 Experimental Evaluation 6 Related Work 7 Conclusions References Compositional Verification of Stigmergic Collective Systems 1 Introduction 2 Background 3 Parallel Emulation Programs 4 Value Analysis of LAbS Specifications 5 Compositional Verification Workflow 6 Related Work 7 Conclusion and Future Work References Efficient Interprocedural Data-Flow Analysis Using Treedepth and Treewidth 1 Introduction 2 The IFDS Framework 3 Treewidth and Treedepth 4 Our Parameterized Algorithm 5 Experimental Results 6 Conclusion References Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization 1 Introduction 2 Preliminaries 3 Problem Definition 4 Key Idea: An Oracle-Guided Numerical Optimization 4.1 The Optimization Problem 4.2 Solving the Optimization Problem 5 MaRVeL: Computing Maximal Robust Specifications 5.1 The Verify Step 5.2 The Optimize Step 5.3 CEGIS at the Progress Step 5.4 An End-to-End Example 5.5 Correctness and Running Time 6 Evaluation 7 Related Work 8 Conclusion References A Generic Framework to Coarse-Grain Stochastic Reaction Networks by Abstract Interpretation 1 Introduction 2 First Case Study: Birth and Death Model 2.1 Reaction Network 2.2 Logical Model 2.3 Formal Derivation of a Coarse-Grained Model 3 General Case 3.1 Concrete Semantics 3.2 Abstract Semantics 3.3 Recovering Information About Transition Probabilities 4 Second Case Study: Competition for Resources 4.1 Reaction Network 4.2 Logical Model 4.3 Formal Discretization of the Reaction Network 5 Conclusion References CosySEL: Improving SAT Solving Using Local Symmetries 1 Introduction 2 State of the Art and Some Definitions 2.1 Basics on Boolean Satisfiability 2.2 Symmetry Group of a Formula 2.3 (Effective) Symmetry Breaking 2.4 Symmetric (Explanation) Learning 3 The Proposed Technique 3.1 Theoretical Foundations and Practical Considerations 3.2 Algorithm 4 Tooling and Evaluation 4.1 Tool Usage 4.2 Evaluation 5 Conclusion References Sound Symbolic Execution via Abstract Interpretation and Its Application to Security 1 Introduction 2 Language and Noninterference Security Notion 3 Overview 4 SoundSE: Sound Symbolic Execution 5 RedSoundSE: Sound SE Combined with Abstract States 6 SoundRSE: Sound Relational Symbolic Execution 7 RedSoundRSE: Product of SoundRSE with Dependence AI 8 Comparison 9 Related Work 10 Conclusion A Trace of Program [f:1:ex]2(d) with RedSoundSE Using Intervals B SE Step Relation C SoundSE Step Relation D Abstract Step Relation E RedSoundSE Step Relation F RSE and SoundRSE Step Relations G RedSoundRSE Step Relation References Result Invalidation for Incremental Modular Analyses 1 Introduction 2 Background 2.1 Modular Static Analysis 2.2 Incremental Modular Static Analysis 3 Strategies for Precision Recovery 3.1 Invalidation Principle 3.2 Component Invalidation (CI) 3.3 Dependency Invalidation (DI) 3.4 Write Invalidation (WI) 4 Evaluation 4.1 Experimental Design 4.2 Precision Evaluation (RQ1) 4.3 Performance w.r.t. No Invalidation (RQ2) 4.4 Performance w.r.t. Full Reanalysis (RQ3) 5 Related Work 6 Conclusion References Synthesizing History and Prophecy Variables for Symbolic Model Checking 1 Introduction 2 Related Work 3 Preliminaries 4 Theory Abstraction and Refinement 4.1 Refinement 5 Counterexample-Guided Refinement 5.1 Refinement with Local Axiom Instances 6 Proof-Based Prophecy Heuristic 7 Capture Conditions from Interpolants 8 Evaluation 8.1 Implementations 8.2 Experiments 9 Conclusion and Future Work References Solving Constrained Horn Clauses over Algebraic Data Types 1 Introduction 2 Preliminaries 3 Recursive Functional Synthesis 3.1 From CHC to FS 3.2 The Eq-Prop Transformation 4 Recursive Invariants 5 Solving CHCs over ADTs 5.1 Challenges of Recursive Functional Synthesis When Dealing with Arbitrary CHCs 5.2 Core Algorithm 6 Automated Induction with AdtInd 6.1 Overview 6.2 Extracting Common Subterms for Helper Lemmas 6.3 Filtering Procedure 7 Implementation and Evaluation 7.1 Framework 7.2 Experiments 8 Related Work 9 Conclusion and Future Work References ARENA: Enhancing Abstract Refinement for Neural Network Verification 1 Introduction 2 Overview 2.1 Spurious Region Guided Refinement 2.2 Scaling up with Multiple Adversarial Label Elimination 3 Methodologies 3.1 Multi-ReLU Network Encoding 3.2 Multiple Adversarial Label Elimination 3.3 Adversarial Example Detection 3.4 The Verification Framework ARENA 4 Experiments 4.1 Experiment Setup 4.2 Comparison with the CPU-Based Verifiers 4.3 Comparison with the GPU-Based Verifier , -CROWN 4.4 Multi-adversarial Label Parameter Study 5 Discussion 6 Related Work 7 Conclusion References Author Index