Cover Image

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

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 II
  • Decision Procedures
  • Bitwuzla
  • 1 Introduction
  • 2 Architecture
  • 2.1 Node Manager
  • 2.2 Solving Context
  • 3 Theory Solvers
  • 3.1 Arrays
  • 3.2 Bit-Vectors
  • 3.3 Floating-Point Arithmetic
  • 3.4 Uninterpreted Functions
  • 3.5 Quantifiers
  • 4 Evaluation
  • 5 Conclusion
  • References
  • Decision Procedures for Sequence Theories
  • 1 Introduction
  • 2 Motivating Example
  • 3 Models
  • 4 Solving Equational and Regular Constraints
  • 5 Algorithm for Straight-Line Formulas
  • 6 Extensions and Undecidability
  • 7 Implementations, Optimizations and Benchmarks
  • 8 Conclusion and Future Work
  • References
  • Exploiting Adjoints in Property Directed Reachability Analysis
  • 1 Introduction
  • 2 Preliminaries and Notation
  • 3 Adjoint PDR
  • 3.1 Progression
  • 3.2 Heuristics
  • 3.3 Negative Termination
  • 4 Recovering Adjoints with Lower Sets
  • 4.1 AdjointPDR"3223379 : Positive Chain in L, Negative Sequence in L"3223379
  • 4.2 AdjointPDR"3223379 Simulates LT-PDR
  • 5 Instantiating AdjointPDR"3223379 for MDPs
  • 6 Implementation and Experiments
  • References
  • Fast Approximations of Quantifier Elimination
  • 1 Introduction
  • 2 Background
  • 3 Extracting Formulas from Egraphs
  • 4 Quantifier Reduction
  • 5 Model Based Projection Using QEL
  • 6 Evaluation
  • 7 Conclusion
  • References
  • Local Search for Solving Satisfiability of Polynomial Formulas
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Notation
  • 2.2 A General Local Search Framework
  • 3 The Search Space of SMT(NRA)
  • 4 The Cell-Jump Operation
  • 4.1 Sample Points
  • 4.2 Cell-Jump Along a Line Parallel to a Coordinate Axis
  • 4.3 Cell-Jump Along a Fixed Straight Line
  • 5 Scoring Functions
  • 6 The Main Algorithm
  • 7 Experiments
  • 7.1 Experiment Preparation
  • 7.2 Instances
  • 7.3 Experimental Results
  • 8 Conclusion.
  • References
  • Partial Quantifier Elimination and Property Generation
  • 1 Introduction
  • 2 Basic Definitions
  • 3 Property Generation by PQE
  • 3.1 High-Level View of Property Generation by PQE
  • 3.2 Property Generation as Generalization of Testing
  • 3.3 Computing Properties Efficiently
  • 3.4 Using Design Coverage for Generation of Unwanted Properties
  • 3.5 High-Quality Tests Specified by a Property Generated by PQE
  • 4 Invariant Generation by PQE
  • 4.1 Bugs Making States Unreachable
  • 4.2 Proving Operative State Unreachability by Invariant Generation
  • 5 Introducing EG-PQE
  • 5.1 An Example
  • 5.2 Description of EG-PQE
  • 5.3 Discussion
  • 6 Introducing EG-PQE+
  • 6.1 Main Idea
  • 6.2 Discussion
  • 7 Experiment with FIFO Buffers
  • 7.1 Buffer Description
  • 7.2 Bug Detection by Invariant Generation
  • 7.3 Detection of the Bug by Conventional Methods
  • 8 Experiments with HWMCC Benchmarks
  • 8.1 Experiment 1
  • 8.2 Experiment 2
  • 8.3 Experiment 3
  • 9 Properties Mimicking Symbolic Simulation
  • 10 Some Background
  • 11 Conclusions and Directions for Future Research
  • References
  • Rounding Meets Approximate Model Counting
  • 1 Introduction
  • 2 Notation and Preliminaries
  • 2.1 Universal Hash Functions
  • 2.2 Helpful Combinatorial Inequality
  • 3 Related Work
  • 4 Weakness of ApproxMC
  • 5 Rounding Model Counting
  • 5.1 Algorithm
  • 5.2 Repetition Reduction
  • 5.3 Proof of Lemma 4 for Case 2-1&lt
  • 1
  • 6 Experimental Evaluation
  • 6.1 RQ1. Overall Performance
  • 6.2 RQ2. Approximation Quality
  • 7 Conclusion
  • A Proof of Proposition 1
  • B Weakness of Proposition 3
  • C Proof of pmax 0.36 for ApproxMC
  • D Proof of Lemma 4
  • D.1 Proof of Pr[L] 0.262 for &lt
  • 2-1
  • D.2 Proof of Pr[L] 0.085 for 1&lt
  • 3
  • D.3 Proof of Pr[L] 0.055 for 3&lt
  • 42-1
  • D.4 Proof of Pr[L] 0.023 for 42-1
  • D.5 Proof of Pr[U] 0.169 for &lt
  • 3.
  • D.6 Proof of Pr[U] 0.044 for 3
  • References
  • Satisfiability Modulo Finite Fields
  • 1 Introduction
  • 1.1 Related Work
  • 2 Background
  • 2.1 Algebra
  • 2.2 Ideal Membership
  • 2.3 Zero Knowledge Proofs
  • 2.4 SMT
  • 3 The Theory of Finite Fields
  • 4 Decision Procedure
  • 4.1 Algebraic Reduction
  • 4.2 Incomplete Unsatisfiability and Cores
  • 4.3 Completeness Through Model Construction
  • 5 Implementation
  • 6 Benchmark Generation
  • 6.1 Examples
  • 7 Experiments
  • 7.1 Comparison with Bit-Vectors
  • 7.2 The Cost of Field Polynomials
  • 7.3 The Benefit of UNSAT Cores
  • 7.4 Comparison to Pure Computer Algebra
  • 7.5 Main Experiment
  • 8 Discussion and Future Work
  • A Proofs of IdealCalc Properties
  • B Proof of Correctness for FindZero
  • C Benchmark Generation
  • References
  • Solving String Constraints Using SAT
  • 1 Introduction
  • 2 Preliminaries
  • 3 Overview
  • 4 Reducing the Alphabet
  • 5 Propositional Encodings
  • 5.1 Substitutions
  • 5.2 Theory Literals
  • 6 Refining Upper Bounds
  • 6.1 Unsatisfiable-Core Analysis
  • 7 Implementation
  • 8 Experimental Evaluation
  • 9 Conclusion
  • References
  • The GOLEM Horn Solver
  • 1 Introduction
  • 2 Tool Overview
  • 3 Back-end Engines of GOLEM
  • 3.1 Transition Power Abstraction
  • 3.2 Engines for State-of-the-Art Model-Checking Algorithms
  • 4 Experiments
  • 4.1 Category LRA-TS
  • 4.2 Category LIA-Lin
  • 4.3 Category LIA-Nonlin
  • 5 Conclusion
  • References
  • Model Checking
  • CoqCryptoLine: A Verified Model Checker with Certified Results
  • 1 Introduction
  • 2 CoqCryptoLine
  • 2.1 CryptoLine Language
  • 2.2 The Architecture of CoqCryptoLine
  • 2.3 Features and Optimizations
  • 3 Walkthrough
  • 4 Evaluation
  • 5 Conclusion
  • References
  • Incremental Dead State Detection in Logarithmic Time
  • 1 Introduction
  • 2 Guided Incremental Digraphs
  • 2.1 Problem Statement.
  • 2.2 Existing Approaches
  • 3 Algorithms
  • 3.1 First-Cut Algorithm
  • 3.2 Logarithmic Algorithm
  • 3.3 Lazy Algorithm
  • 4 Experimental Evaluation
  • 5 Application to Extended Regular Expressions
  • 5.1 Reduction from Incremental Regex Emptiness to GIDs
  • 6 Related Work
  • References
  • Model Checking Race-Freedom When ``Sequential Consistency for Data-Race-Free Programs'' is Guaranteed
  • 1 Introduction
  • 2 Theory
  • 3 Implementation and Evaluation
  • 3.1 Background on OpenMP
  • 3.2 Background on CIVL-C
  • 3.3 Transformation for Data Race Detection
  • 3.4 Evaluation
  • 4 Related Work
  • 5 Conclusion
  • References
  • Searching for i-Good Lemmas to Accelerate Safety Model Checking
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Boolean Transition System
  • 2.2 Safety Checking and Reachability Analysis
  • 2.3 Overview of IC3 and CAR
  • 3 Finding i-Good Lemmas
  • 3.1 What Are i-good Lemmas
  • 3.2 Searching for i-good Lemmas
  • 4 Related Work
  • 5 Evaluation
  • 5.1 Experimental Setup
  • 5.2 Experimental Results
  • 5.3 Why Do branching and refer-skipping Work?
  • 6 Conclusions and Future Work
  • References
  • Second-Order Hyperproperties
  • 1 Introduction
  • 2 Preliminaries
  • 3 Second-Order HyperLTL
  • 3.1 Hyper2LTL
  • 3.2 Hyper2LTLfp
  • 3.3 Common Knowledge in Multi-agent Systems
  • 3.4 Hyper2LTL Model Checking
  • 4 Expressiveness of Hyper2LTL
  • 4.1 Hyper2LTL and LTLK, C
  • 4.2 Hyper2LTL and Asynchronous Hyperproperties
  • 5 Model-Checking Hyper2LTLfp
  • 5.1 Fixpoints in Hyper2LTLfp
  • 5.2 Functions as Automata
  • 5.3 Model Checking for First-Order Quantification
  • 5.4 Bidirectional Model Checking
  • 5.5 Computing Under- and Overapproximations
  • 6 Implementation and Experiments
  • 7 Related Work
  • 8 Conclusion
  • References
  • Neural Networks and Machine Learning
  • Certifying the Fairness of KNN in the Presence of Dataset Bias
  • 1 Introduction.
  • 2 Background
  • 2.1 Fairness of the Learned Model
  • 2.2 Fairness in the Presence of Dataset Bias
  • 3 Overview of Our Method
  • 3.1 The KNN Algorithm
  • 3.2 Certifying the KNN Algorithm
  • 4 Abstracting the KNN Prediction Step
  • 4.1 Finding the K-Nearest Neighbors
  • 4.2 Checking the Classification Result
  • 5 Abstracting the KNN Learning Step
  • 5.1 Overapproximating the Classification Error
  • 5.2 Underapproximating the Classification Error
  • 6 Experiments
  • 7 Related Work
  • 8 Conclusions
  • References
  • Monitoring Algorithmic Fairness
  • 1 Introduction
  • 1.1 Motivating Examples
  • 1.2 Related Work
  • 2 Preliminaries
  • 2.1 Markov Chains as Randomized Generators of Events
  • 2.2 Randomized Register Monitors
  • 3 Algorithmic Fairness Specifications and Problem Formulation
  • 3.1 Probabilistic Specification Expressions
  • 3.2 The Monitoring Problem
  • 4 Frequentist Monitoring
  • 4.1 The Main Principle
  • 4.2 Implementation of the Frequentist Monitor
  • 5 Bayesian Monitoring
  • 5.1 The Main Principle
  • 5.2 Implementation of the Bayesian Monitor
  • 6 Experiments
  • 7 Conclusion
  • References
  • nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
  • 1 Introduction
  • 2 Background and Related Work
  • 2.1 Natural Language to Linear-Time Temporal Logic
  • 2.2 Large Language Models
  • 3 The nl2spec Framework
  • 3.1 Overview
  • 3.2 Interactive Few-Shot Prompting
  • 4 Evaluation
  • 4.1 Study Setup
  • 4.2 Results
  • 5 Conclusion
  • References
  • NNV 2.0: The Neural Network Verification Tool
  • 1 Introduction
  • 2 Related Work
  • 3 Overview and Features
  • 3.1 NNV 2.0 vs NNV
  • 4 Evaluation
  • 4.1 Comparison to MATLAB's Deep Learning Verification Toolbox
  • 4.2 Neural Ordinary Differential Equations
  • 4.3 Recurrent Neural Networks
  • 4.4 Semantic Segmentation
  • 5 Conclusions
  • References.
  • QEBVerif: Quantization Error Bound Verification of Neural Networks.

Similar Items