Cover Image

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

Bibliographic Details
Main Author: Enea, Constantin.
Other Authors: Lal, Akash.
Format: eBook
Language:English
Published: Cham : Springer, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
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.

Similar Items