Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part II (Lecture Notes in Computer Science)

Preface
Organization
Contents – Part II
Contents – Part I
Probabilistic Techniques
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
1 Introduction
2 Preliminaries
3 Overview of Our Approach
3.1 Naïve Solution
3.2 Improved Solution
4 Algorithm for Discrete-Time MDP
5 Algorithm for Continuous-Time MDP
6 Experimental Results
7 Conclusion
References
Sampling-Based Verification of CTMCs with Uncertain Rates
1 Introduction
2 Problem Statement
3 Precise Sampling-Based Prediction Regions
3.1 Constructing Prediction Regions
3.2 Bounding the Containment Probability
3.3 An Algorithm for Computing Prediction Regions
4 Imprecise Sampling-Based Prediction Regions
4.1 Prediction Regions on Imprecise Solutions
4.2 Computing the Complexity
4.3 Solution Refinement Scheme
5 Batch Verification for CTMCs
6 Experiments
7 Related Work
8 Conclusion
References
Playing Against Fair Adversaries in Stochastic Games with Total Rewards
1 Introduction
2 Roborta vs. the Fair Light (A Motivating Example)
3 Preliminaries
4 Stopping Games and Fair Strategies
5 Experimental Validation
6 Related Work
7 Concluding Remarks
References
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
1 Introduction
2 Overview of Our Approach and Results
2.1 Introductory Example
2.2 Overview of Benchmarks and Results
3 Probabilistic Functional Language
4 Operational Semantics
5 Type-and-Effect System for Expected Cost Analysis
5.1 Resource Functions
5.2 Typing Rules
5.3 Soundness Theorems
6 Implementation and Evaluation
7 Conclusion
References
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
1 Introduction
2 Model-Based API Fuzzing for SMT Solvers
3 Murxla
3.1 The Core
3.2 API Fuzzer
3.3 Solver Wrappers
3.4 Tracer, Untracer, Trace Minimizer
4 Evaluation
5 Conclusion
References
Automata and Logic
FORQ-Based Language Inclusion Formal Testing
1 Introduction
2 Preliminaries
3 Foundations of Our Approach
4 Defining FORQs from the Structure of an Automaton
5 A FORQ-Based Inclusion Algorithm
6 Complexity of the Structural FORQ-Based Algorithm
7 Implementation and Experiments
7.1 Experimental Evaluation
8 Discussions
9 Conclusion and Future Work
References
Sound Automation of Magic Wands
1 Introduction
2 Background and Motivation
2.1 Implicit Dynamic Frames
2.2 A Typical Example Using Magic Wands
2.3 Wand Ghost Operations
2.4 The Footprint Inference Attempt (FIA)
3 A Logical Framework for Packaging Wands
3.1 Footprint Selection Strategies
3.2 Package Logic: Preliminaries
3.3 The Package Logic
3.4 Soundness and Completeness
3.5 A Sound Package Algorithm
4 Using the Logic with Combinable Wands
5 Evaluation
6 Related Work
7 Conclusion
References
Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition
1 Introduction
2 Preliminaries
3 Determinization Algorithms of SCCs
3.1 Successor Computation Inside IWCs
3.2 Successor Computation Inside DACs
3.3 Successor Computation Inside NACs
4 Determinization of NBAs to DELAs
5 Empirical Evaluation
6 Related Work
7 Conclusion and Future Work
References
From Spot 2.0 to Spot 2.10: What's New?
1 Availability, Purpose, and Evolution
2 Use-cases of Spot, and Related Tools
3 Automata Representation
4 Introduction of Alternating Automata
5 Extending Automata via Named Properties
6 Games, Mealy Machines, and LTL Synthesis
7 Online Application for LTL Formulas
8 Shortcomings and One Future Direction
References
Complementing Büchi Automata with Ranker
1 Introduction
2 Büchi Automata
3 Architecture
3.1 Preprocessing and Postprocessing
3.2 Complementation Approaches
4 Optimizations of the Constructions
4.1 Macrostates Adjustment for Inherently Weak Automata
4.2 NCSB-MaxRank Construction
5 Experimental Evaluation
5.1 Effect of the Proposed Optimizations
5.2 Comparison with Other Tools
References
Deductive Verification and Decision Procedures
Even Faster Conflicts and Lazier Reductions for String Solvers
1 Introduction
1.1 Related Work
2 Preliminaries
3 Eager Equality-Based Conflicts for Strings
3.1 Enhancing Congruence Closure with Evaluation
3.2 Tracking Properties of Equivalence Classes
4 Model-Based Reductions for Strings
5 Fast Techniques for Regular Expression Inclusion
6 An Extended Strategy for Strings in CDCL(T)
7 Evaluation
8 Conclusion
References
Local Search for SMT on Linear Integer Arithmetic
1 Introduction
2 Preliminary
3 A Local Search Framework for SMT (LIA)
4 The Critical Move Operator and a Two-Level Heuristic
4.1 Critical Move
4.2 A Two-Level Heuristic
5 Scoring Functions
6 LS-LIA Algorithm
7 Experiments
7.1 Experiment Preliminaries
7.2 Results on SMTLIB-LIA and SMTLIB-IDL Benchmarks
7.3 Results on Job Shop Scheduling Benchmark
7.4 Results on RVPredict Benchmark
7.5 Effectiveness of Proposed Strategies
8 Conclusion and Future Work
References
Reasoning About Data Trees Using CHCs
1 Introduction
2 Data Trees
3 Monadic Second-Order Logic with Data
4 Symbolic Data-Tree Automata
5 Solving the Emptiness Problem for Sdtas
6 From Logic to Automata
6.1 Building the Enumerated Tree Automaton
6.2 Building the Symbolic Data Tree Automaton
6.3 Supporting Auxiliary Data
7 Implementation and Experiments
7.1 Proving Properties of Tree Data Structures
7.2 Solving an Infinite-State Game
8 Related Work
9 Conclusions and Future Directions
References
Verified Erasure Correction in Coq with MathComp and VST
1 Introduction
1.1 Forward Erasure Correction
1.2 Coq and VST
2 The RSE Algorithm
2.1 Initialization
2.2 Encoding
2.3 Decoding
3 Verification Structure
4 Functional Model
4.1 The Encoder and Decoder
4.2 Gaussian Elimination
4.3 Field Operations
5 Verifying the Functional Model
5.1 Decoder Correctness
5.2 Gaussian Elimination
6 Verifying the Implementation
6.1 Implementation Differences from Algorithm
6.2 Implementation-Specific Verification Challenges
6.3 VST Specifications
6.4 Verifying fecgeneratemathtables
6.5 Verifying fecblkdecode
6.6 Implementation Bug
7 Related Work
8 Future Work
9 Conclusion
References
End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
1 Introduction
2 Contributions
3 Background
4 A Workflow for End-to-End Verification in Coq
5 A Proof-Oriented Virtual Machine Model
5.1 Proof of Software-Fault Isolation
6 A Synthesis-Oriented eBPF Interpreter
7 Simulation Proof of the C rBPF Virtual Machine
8 CertrBPF Verifier
9 Evaluation: Case Study of RIOT's Femto-Containers
10 Related Works
11 Conclusion and Future Works
References
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
1 Introduction
2 A Motivating Example
3 The Hemiola Domain-Specific Language
3.1 Syntax
3.2 Rule Templates
4 Verification in Hemiola
4.1 Semantics of the Hemiola DSL
4.2 Serializability in Hemiola
4.3 Predicate Messages
4.4 Serializability Guarantee by the Hemiola DSL
5 Case Studies: Hierarchical MSI and MESI Protocols
5.1 Cache States
5.2 Protocol Description with Rule Templates
5.3 Invariant Proof Using Predicate Messages
6 Compilation and Synthesis to Hardware
6.1 Compilation of Hemiola Protocols
6.2 Synthesis of Hemiola Protocols
7 Related Work
8 Conclusion
References
Machine Learning
Specification-Guided Learning of Nash Equilibria with High Social Welfare
1 Introduction
1.1 Related Work
2 Preliminaries
2.1 Markov Game
2.2 Specification Language
2.3 Abstract Graphs
2.4 Nash Equilibrium and Social Welfare
3 Overview
4 Prioritized Enumeration
4.1 Product Abstract Graph
4.2 Compositional RL Algorithm
5 Nash Equilibria Verification
5.1 Problem Formulation
5.2 High-Level Procedure
5.3 Reduction to Min-Max Games
5.4 Solving Min-Max Games
6 Complexity
7 Experiments
8 Conclusions
References
Synthesizing Fair Decision Trees via Iterative Constraint Solving
1 Introduction
2 Background
2.1 Training Dataset E
2.2 Decision Tree Learning
2.3 Fairness Metric
3 Our Method
3.1 The Objective Function O
3.2 Encoding of the Decision Tree (tree)
3.3 Encoding of the Accuracy Requirement (accu)
3.4 Encoding of the Fairness Requirement
4 Generalization and Performance Enhancement
4.1 Relating to Existing Algorithms
4.2 Performance Enhancement
4.3 Encoding Other Group Fairness Metrics
5 Experiments
6 Related Work
7 Conclusion
References
SMT-Based Translation Validation for Machine Learning Compiler
1 Introduction
2 Multi-level Intermediate Representation (MLIR)
3 Overview
3.1 Abstraction for Floating-Point Arithmetic
3.2 The Formal Semantics of Dialects
4 Encoding Floating-Point Numbers and Tensors
4.1 Abstract Domain of Floating-Point Numbers
4.2 Encoding Tensors
4.3 Calculating the Bit Width
5 Supporting Tensor Operations and Loops
5.1 Encoding Tensor Operations
5.2 Encoding Loops
5.3 Supporting Arithmetic Properties of Reductions
6 Encoding Memory and Refinement
6.1 Memory Model
6.2 Encoding the Memory Model
6.3 Compiler Correctness and Abstraction Refinement
7 Implementation and Evaluation
7.1 Validating MLIR Unit Tests
7.2 Validating Compilation of Deep Learning Models
7.3 Performance Evaluation of Hash-Based Encoding
8 Related Work
9 Conclusion
References
Verifying Fairness in Quantum Machine Learning
1 Introduction
1.1 Related Works and Challenges
2 Quantum Decision Models
3 Defining Fairness
4 Characterizing Fairness
4.1 Fairness and Lipschitz Constant
4.2 Fairness and Noises
5 Fairness Verification
5.1 Computing the Lipschitz Constant
5.2 Fairness Verification Algorithm
6 Evaluation
6.1 A Practical Application in Finance
6.2 Scalability in the NISQ Era
7 Conclusion
References
MoGym: Using Formal Models for Training and Verifying Decision-making Agents
1 Introduction
2 Formal Models as Training Environments
3 Verifying Agents Using Statistical Model Checking
4 Experimental Insights
5 Conclusion and Future Work
References
Synthesis and Concurrency
Synthesis and Analysis of Petri Nets from Causal Specifications
1 Introduction
2 The Causal Semantics of Petri Nets
3 Message Sequence Chart Languages
4 Slice Automata
5 Weak Saturation
6 Slice Traces
7 From MSC Automata to Slice Automata
8 From Mazurkiewicz Traces to Slice Languages
9 Conclusion
References
Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations
1 Introduction
2 Preliminaries
2.1 Petri Nets
2.2 Workflow Nets
3 Reachability Relaxations
3.1 Preservation Under Reduction Rules
4 Using Relaxations For Generalised Soundness
4.1 Integer Unboundedness
4.2 Continuous Soundness
5 Using Relaxations For Structural Soundness
6 Free-Choice Workflow Nets
7 Experimental Evaluation
7.1 Free-Choice Benchmark Suite
7.2 Synthetic Instances
8 Conclusion
References
Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET
1 Introduction
2 Related Work
3 The FRETish Language
4 Implementation
5 Features Walkthrough
6 Case Studies
6.1 Lift Plus Cruise Aircraft
6.2 Generic Infusion Pump
7 Conclusion
References
Information Flow Guided Synthesis
1 Introduction
2 The Bit Transmission Problem
3 Preliminaries
4 Necessary Information Flow in Distributed Systems
4.1 Necessary Information Flow
4.2 Time-Bounded Information Flow
5 Compositional Synthesis
5.1 Constructing the Hyper Implementations
5.2 Composition of Hyper Implementations
6 A More Practical Approach
7 Experiments
8 Related Work
9 Conclusion
References
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
1 Introduction
2 Overview and Problem Definition
2.1 Motivating Examples
2.2 Problem Definition
3 Feasibility Conditions and the Greedy Construction
4 Exact LQCI for Automata Specifications
5 Approximate LQCI for Symbolic Specifications
6 Maximum-Entropy LQCI
7 Experiments
8 Conclusion
References
Author Index