Computer Aided Verification : : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III.

• Superior document: Lecture Notes in Computer Science Series ; v.13966
• Author: Enea, Constantin.
• TeilnehmendeR: Lal, Akash.
• Place / Publishing House: Cham : : Springer,, 2023.; ©2023.
• Year of Publication: 2023
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (513 pages)

Table of Contents

Intro -- Preface -- Organization -- Contents - Part III -- Probabilistic Systems -- A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties -- 1 Introduction -- 2 Theoretical Background -- 2.1 Solving Rabin Games Symbolically -- 2.2 Computing Symbolic Controllers for Stochastic Dynamical Systems -- 3 Implementation Details -- 3.1 Genie -- 3.2 FairSyn -- 3.3 Mascot-SDS -- 4 Examples -- 4.1 Synthesizing Code-Aware Resource Mangers Using FairSyn -- 4.2 Synthesizing Controllers for Stochastic Dynamical Systems Using Mascot-SDS -- References -- Automated Tail Bound Analysis for Probabilistic Recurrence Relations -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Recurrence Relations -- 3 Exponential Tail Bounds via Markov's Inequality -- 4 An Algorithmic Approach -- 4.1 The Guess Procedure Guess(f,t) -- 4.2 The Check Procedure CheckCond(cf,ct) -- 5 Experimental Results -- 6 Related Work -- References -- Compositional Probabilistic Model Checking with String Diagrams of MDPs -- 1 Introduction -- 2 String Diagrams of MDPs -- 2.1 Outline -- 2.2 Open MDPs -- 2.3 Rightward Open MDPs and Traced Monoidal String Diagrams -- 2.4 TSMC Equations Between roMDPs -- 2.5 Open MDPs and ``Compact Closed'' String Diagrams -- 3 Decomposition Equalities for Open Markov Chains -- 4 Semantic Categories and Solution Functors -- 4.1 Semantic Category for Rightward Open MCs -- 4.2 Semantic Category of Rightward Open MDPs -- 4.3 Semantic Category of MDPs -- 5 Implementation and Experiments -- References -- Efficient Sensitivity Analysis for Parametric Robust Markov Chains -- 1 Introduction -- 2 Overview -- 3 Formal Problem Statement -- 4 Differentiating Solution Functions for pMCs -- 4.1 Computing Derivatives Explicitly -- 4.2 Computing k-Highest Derivatives -- 5 Differentiating Solution Functions for prMCs.

5.1 Computing Derivatives via pMCs (and When It Does Not Work) -- 5.2 Computing Derivatives Explicitly -- 5.3 Computing k-Highest Derivatives -- 6 Numerical Experiments -- 7 Related Work -- 8 Concluding Remarks -- References -- MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 2.1 Markov Systems -- 2.2 MDPs as Distribution Transformers -- 3 Problem Statement and Examples -- 4 Proving Safety by Invariants -- 4.1 Distribution Strategies -- 4.2 Distributional Invariants for MDP Safety -- 5 Algorithms for Distributional Invariant Synthesis -- 5.1 Synthesis of Affine Invariants and Memoryless Strategies -- 5.2 Synthesis of Affine Invariants and General Strategies -- 6 Discussion, Extensions, and Variants -- 7 Implementation and Evaluation -- 8 Conclusion -- References -- Search and Explore: Symbiotic Policy Synthesis in POMDPs -- 1 Introduction -- 2 Motivating Examples -- 3 Preliminaries and Problem Statement -- 4 FSCs for and from Belief Exploration -- 4.1 Belief Exploration with Explicit FSC Construction -- 4.2 Using FSCs for Cut-Off Values -- 4.3 Extracting FSC from Belief Exploration -- 5 Accelerated Inductive Synthesis -- 5.1 Inductive Synthesis with k-FSCs -- 5.2 Using Reference Policies to Accelerate Inductive Synthesis -- 5.3 Inductive Synthesis with Adequate FSCs -- 6 Integrating Belief Exploration with Inductive Synthesis -- 7 Experiments -- 8 Conclusion and Future Work -- References -- Security and Quantum Systems -- AutoQ: An Automata-Based Quantum Circuit Verifier -- 1 Introduction -- 2 Tree Automata-Based Verification of Quantum Circuits -- 2.1 High-Level Specification Language -- 2.2 Complex Number Representation -- 2.3 Precise Semantics of the Specification -- 3 Entailment Checking -- 4 Architecture -- 5 Use Cases.

5.1 Hadamard Square is Identity -- 5.2 Zero Imaginary Part of Amplitudes -- 5.3 Probability of Measuring the Correct Answer -- 5.4 Increasing Amplitude of the Correct Answer -- 6 Conclusion -- References -- Bounded Verification for Finite-Field-Blasting -- 1 Introduction -- 1.1 Related Work -- 2 Background -- 2.1 Logic -- 2.2 Zero Knowledge Proofs -- 2.3 Compilation Targeting Zero Knowledge Proofs -- 3 Overview and Example -- 3.1 An Example of Field-Blasting -- 3.2 Key Ideas -- 4 Architecture -- 4.1 Encodings -- 4.2 Encoding Rules -- 4.3 Calculus -- 5 Verification Conditions -- 5.1 Correctness Definition -- 5.2 Rule VCs -- 5.3 A Correct Field-Blasting Calculus -- 6 Case Study: A Verifiable Field-Blaster for CirC -- 6.1 Verification Evaluation -- 6.2 Performance and Output Quality Evaluation -- 7 Discussion -- A Zero-Knowledge Proofs and Compilers -- B Compiler Correctness Proofs -- C CirC-IR -- D Optimizations to the CirC Field-Blaster -- E Verified Field-Blaster Performance Details -- F Verifier Performance Details -- G Bugs Found in the CirC Field Blaster -- References -- Formally Verified EVM Block-Optimizations -- 1 Introduction -- 2 Background -- 3 EVM Semantics in Coq -- 4 Formal Verification of EVM-Optimizations in Coq -- 4.1 EVM Symbolic Execution in Coq -- 4.2 Simplification Rules -- 4.3 Stacks Equivalence Modulo Commutativity -- 5 Implementation and Experimental Evaluation -- 6 Conclusions, Related and Future Work -- References -- SR-SFLL: Structurally Robust Stripped Functionality Logic Locking -- 1 Introduction -- 2 Background -- 2.1 Stripped Functionality Logic Locking (SFLL) -- 2.2 SFLL Attacks -- 2.3 Analysis of the Structural Attacks on SFLL -- 3 Overview -- 3.1 Preliminaries -- 3.2 Approach -- 4 SR-SFLL -- 4.1 Problem Statement -- 4.2 Intuition: SR-SFLL -- 4.3 Methodology: SR-SFLL -- 5 SyntAk -- 6 Evaluation.

6.1 Robustness of SR-SELL(0) and SR-SELL on Existing Attacks -- 6.2 Robustness of SR-SELL(0) and SR-SELL on SyntAk -- 6.3 Overhead of SR-SELL(0) and SR-SELL -- 7 Related Work -- 8 Conclusions -- References -- Symbolic Quantum Simulation with Quasimodo -- 1 Introduction -- 2 Background on Quantum Simulation -- 3 Quasimodo's Programming and Analysis Interface -- 3.1 Extending Quasimodo -- 4 The Internals of Quasimodo -- 5 Experiments -- 6 Conclusion -- References -- Verifying the Verifier: eBPF Range Analysis Verification -- 1 Introduction -- 2 Background on Abstract Interpretation -- 3 Abstract Interpretation in the Linux Kernel -- 4 Automatic Verification of the Kernel's Algorithms -- 4.1 Soundness Specification for Abstraction/Reduction Operators -- 4.2 Refining Soundness Specification with Input Preconditioning -- 4.3 Automatically Producing Programs Exercising Soundness Bugs -- 5 C to Logic for Kernel's Abstract Operators -- 6 Experimental Evaluation -- 7 Limitations and Caveats -- 8 Related Work -- 9 Conclusion -- References -- Software Verification -- Automated Verification of Correctness for Masked Arithmetic Programs -- 1 Introduction -- 2 Preliminaries -- 3 The Core Language -- 4 Overview of the Approach -- 4.1 Our Approach -- 5 Term Rewriting System -- 6 Algorithmic Verification -- 6.1 Term Normalization Algorithm -- 6.2 Computing Affine Constants -- 6.3 Verification Algorithm -- 6.4 Implementation Remarks -- 7 Evaluation -- 7.1 Evaluation for Computing Affine Constants -- 7.2 Evaluation for Correctness Verification -- 7.3 Scalability of FISCHER -- 7.4 Evaluation for More Boolean Masking Schemes -- 7.5 Evaluation for Arithmetic/Boolean Masking Conversions -- 8 Conclusion -- References -- Automatic Program Instrumentation for Automatic Verification -- 1 Introduction -- 2 Instrumentation Framework -- 2.1 The Core Language.

2.2 Instrumentation Operators -- 2.3 Instrumentation Correctness -- 3 Instrumentation Application Strategies -- 4 Instrumentation Operators for Arrays -- 4.1 Instrumentation Operators for Quantification over Arrays -- 4.2 Instrumentation Operators for Aggregation over Arrays -- 5 Evaluation -- 5.1 Implementation -- 5.2 Experiments and Comparisons -- 6 Related Work -- 7 Conclusion -- References -- Boolean Abstractions for Realizability Modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Boolean Abstraction -- 3.1 Notation -- 3.2 The Boolean Abstraction Algorithm -- 3.3 From Local Simulation to Equi-Realizability -- 4 Efficient Algorithms for Boolean Abstraction -- 4.1 Quasi-reactions -- 4.2 Quasi-reaction-based Optimizations -- 4.3 A Single Model-Loop Algorithm (Algorithm 2) -- 4.4 A Nested-SAT Algorithm (Algorithm 3) -- 5 Empirical Evaluation -- 6 Related Work and Conclusions -- References -- Certified Verification for Algebraic Abstraction -- 1 Introduction -- 2 Preliminaries -- 3 ToyLang -- 3.1 Syntax and Semantics -- 4 Algebraic Abstraction -- 4.1 Soundness Conditions -- 4.2 Polynomial Program Verification -- 5 Certified Verification -- 5.1 Verified Abstraction Algorithm -- 5.2 Verification through Certification -- 5.3 Optimization -- 6 Evaluation -- 6.1 Field and Group Operation in Elliptic Curves -- 6.2 Number-Theoretic Transform in Kyber -- 7 Conclusion -- References -- Complete Multiparty Session Type Projection with Automata -- 1 Introduction -- 2 Motivation and Overview -- 3 Preliminaries -- 4 Synthesizing Implementations -- 5 Checking Implementability -- 6 Soundness -- 7 Completeness -- 8 Complexity -- 9 Evaluation -- 10 Discussion -- 11 Related Work -- References -- Early Verification of Legal Compliance via Bounded Satisfiability Checking -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Satisfiability Checking Problem.

4 Checking Bounded Satisfiability.