Computer Aided Verification : : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II.

• Superior document: Lecture Notes in Computer Science Series ; v.14682
• Author: Gurfinkel, Arie.
• TeilnehmendeR: Ganesh, Vijay.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2024.; ©2024.
• Year of Publication: 2024
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (447 pages)

Table of Contents

• Intro
• Preface
• Organization
• Invited Talks
• How to Solve Math Problems Without Talent
• Bridging Formal Mathematics and Software Verification
• The Art of SMT Solving
• Contents - Part II
• Concurrency
• The VerCors Verifier: A Progress Report
• 1 Introduction
• 2 New and Improved Language Support
• 2.1 Improved Existing Language Support
• 2.2 Newly Supported Frameworks
• 2.3 Programming Languages Encoded into VerCors
• 3 VerCors Implementation Changes
• 4 Deriving Verified, Optimised Programs
• 5 Case Studies
• 5.1 Tunnel Control Software Components
• 5.2 Verification of Red-Black Trees and their Parallel Merge
• 5.3 GPU Case Studies
• 5.4 Student Projects
• 6 Conclusions, Related Work and Future Work
• References
• Parsimonious Optimal Dynamic Partial Order Reduction
• 1 Introduction
• 2 Main Concepts
• 3 Programs, Executions, and Equivalence
• 4 Design of the POP Algorithm
• 4.1 Parsimonious Race Reversals
• 4.2 The Parsimonious-OPtimal DPOR (POP) Algorithm
• 4.3 Parsimonious Sleep Set Characterization
• 5 Correctness and Space Complexity
• 6 Implementation and Evaluation
• 7 Related Work
• 8 Conclusion
• References
• Collective Contracts for Message-Passing Parallel Programs
• 1 Introduction
• 2 A Theory of Collective Contracts
• 2.1 Language
• 2.2 Semantics
• 2.3 Collective Correctness
• 2.4 Simulation
• 3 Collective Contracts for C/MPI
• 3.1 Background from MPI
• 3.2 Contract Structure
• 4 Evaluation
• 4.1 Collective Contract Examples
• 4.2 Bounded Verification of Collective Contracts
• 5 Related Work
• 6 Discussion
• References
• Distributed Systems
• mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
• 1 Introduction
• 2 Modeling Language
• 2.1 Benchmarks
• 3 Satisfiability-Based Queries
• 3.1 Queries
• 3.2 Counterexamples.
• 3.3 Decidability and Finite Counterexamples via EPR
• 4 Invariant Inference
• 5 Designing mypyvy's Internals
• 6 Works Using mypyvy
• 7 Related Work
• References
• Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
• 1 Introduction
• 2 Background
• 3 Subsumption-Based Representation of Sets of Formulas
• 3.1 Bounded First-Order Languages
• 3.2 Syntactic Subsumption
• 3.3 Canonicalization
• 3.4 Representing Sets of Formulas
• 4 The Weaken Operator
• 4.1 Weakening a Single Canonical Formula
• 4.2 Weakening Sets of Formulas
• 4.3 Design Consideration and Tradeoffs
• 5 Data Structure for Sets of Formulas
• 6 Implementation and Evaluation
• 6.1 Implementation
• 6.2 Experiments
• 6.3 Results
• 7 Related Work
• 8 Conclusion
• References
• Verifying Cake-Cutting, Faster
• 1 Introduction
• 2 Cake-Cutting Preliminaries
• 3 Language and Type System
• 3.1 Syntax of Base Slice
• 3.2 A Linear Type System for Slice
• 3.3 Semantics
• 3.4 Disjointness
• 4 Constraints
• 5 Piecewise Uniform Reduction
• 5.1 Replicating Protocol Executions
• 5.2 Piecewise Uniform Valuations
• 5.3 Piecewise Uniform Replacement
• 6 Implementation and Evaluation
• 7 Related and Future Work
• References
• Runtime Verification and Monitoring
• General Anticipatory Runtime Verification
• 1 Introduction
• 2 Lola Monitoring Revisited
• 2.1 Recurrent Monitoring
• 2.2 Lola
• 3 Lola Recurrent Online Monitoring Semantics
• 4 An Abstraction Framework for Lola Monitoring
• 5 Abstraction-Based Recurrent Lola Monitoring
• 6 Symbolic Recurrent Lola Monitoring
• 7 Empirical Evaluation
• 8 Conclusion
• References
• Proactive Real-Time First-Order Enforcement
• 1 Introduction
• 2 Preliminaries
• 3 Proactive, Real-Time, First-Order Enforcement
• 3.1 System Model
• 3.2 Enforcers
• 4 Enforceable MFOTL Formulae.
• 5 Enforcing EMFOTL
• 5.1 Obligations
• 5.2 Checking Satisfaction of MFOTL Formulae Under Assumptions
• 5.3 The Enforcement Algorithm
• 5.4 Correctness
• 6 Evaluation
• 7 Related Work
• 8 Conclusion
• References
• Predictive Monitoring with Strong Trace Prefixes
• 1 Introduction
• 2 Predictive Monitoring and Trace Theory
• 3 Strong Trace Prefixes
• 3.1 Modelling Correct Reorderings with Strong Trace Prefixes
• 4 Complexity of Predictive Monitoring
• 4.1 Non-deterministic Predictive Monitoring
• 4.2 Deterministic Predictive Monitoring
• 4.3 Ensuring Well-Formedness and Soundness
• 5 Strong Reads-From Prefixes
• 6 Strong Prefixes Versus Synchronization Preservation
• 7 Experimental Evaluation
• 7.1 Enhanced Predictive Power of Strong Prefixes
• 7.2 Strong Reads-From Prefixes v/s Sync-Preservation
• 8 Related Work and Conclusions
• References
• Case Studies and Tools
• Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned
• 1 Introduction
• 1.1 Related Work
• 2 Stream-Based Monitoring
• 3 Setup
• 3.1 Monitoring Applications
• 3.2 Development Cycle for the Monitor
• 4 Abstract Integration
• 4.1 Common Interfaces
• 5 Concrete Integration of Representative Specifications
• 6 Conclusion
• References
• Testing the Migration from Analog to Software-Based Railway Interlocking Systems
• 1 Introduction
• 2 Operational Setting
• 3 Bridging the Gap Between ReRIS and SwRIS
• 3.1 Simulations Extractor
• 3.2 Working with a Partial ReRIS Model
• 3.3 Mapping a ReRIS Simulation into an Abstract SwRIS Test
• 3.4 Test Execution
• 4 Related Works
• 5 Experimental Evaluation
• 6 Conclusions
• References
• soid: A Tool for Legal Accountability for Automated Decision Making
• 1 Introduction
• 1.1 Related Work
• 2 soid Tool Architecture and Usage
• 2.1 Example #1: Decision Tree Inference.
• 3 soid-gui Architecture and Usage
• 3.1 Example #2: Three Cars on the Stand
• 4 Conclusion
• References
• Machine Learning and Neural Networks
• Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
• 1 Introduction
• 2 Architecture and Core Components
• 2.1 Engine
• 2.2 Context-Dependent Data-Structures
• 2.3 Proof Module
• 2.4 Front End
• 2.5 Availability, License, and Installation
• 3 Highlighted Features and Applications
• 4 Runtime Evaluation
• 5 Conclusion and Next Steps
• References
• Monitizer: Automating Design and Evaluation of Neural Network Monitors
• 1 Introduction
• 2 Related Work
• 3 Monitizer
• 3.1 Overview
• 3.2 Use Cases
• 3.3 Phases of Monitizer
• 3.4 Classification of Out-of-Distribution Data
• 3.5 Library of Monitors, NNs, and Datasets
• 4 Summary of Evaluation by Case Study
• 5 Conclusion
• References
• Guiding Enumerative Program Synthesis with Large Language Models
• 1 Introduction
• 2 Background
• 3 Overview
• 4 Stand-Alone LLM
• 4.1 Prompting the LLM
• 5 Synthesis with pCFG Guidance: pCFG-synth
• 5.1 Inferring a Weighted CFG
• 5.2 Probabilistic Guided Search
• 5.3 Weighted A* Search
• 6 Enumerative Synthesis with an Integrated LLM (iLLM-synth)
• 6.1 Integrated Prompting
• 6.2 Updating the Weighted Grammar
• 6.3 Integrating Syntactic Feedback into Enumerative Search
• 7 Evaluation
• 8 Threats to Validity
• 9 Related Work
• 10 Conclusions
• References
• Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification
• 1 Introduction
• 2 Background and Motivation
• 3 Methodology
• 3.1 Code Decomposition
• 3.2 Hierarchical Specification Generation
• 3.3 Specification Validation
• 4 Evaluation
• 4.1 Evaluation Setup
• 4.2 RQ1. Effectiveness on General Specification
• 4.3 RQ2. Effectiveness on Loop Invariants.
• 4.4 RQ3. Efficiency of AutoSpec
• 4.5 RQ4. Ablation Study
• 4.6 Case Studies
• 5 Threats to Validity
• 6 Related Work
• 7 Conclusion
• References
• Verifying Global Two-Safety Properties in Neural Networks with Confidence
• 1 Introduction
• 2 Background
• 2.1 Feed-Forward Neural Networks
• 2.2 Hyperproperties
• 2.3 Relational Verification and Self-composition
• 2.4 Robustness and Fairness
• 3 Confidence Based Global Verification of Feed-Forward Neural Networks
• 3.1 Encoding 2-Safety Properties as Product Neural Network
• 3.2 Softmax Approximation
• 4 Implementation
• 5 Experimental Evaluation
• 5.1 Discussion
• 6 Conclusion
• References
• Certified Robust Accuracy of Neural Networks Are Bounded Due to Bayes Errors
• 1 Introduction
• 2 Preliminary and Problem Definition
• 2.1 Robustness in Classification
• 2.2 Bayes Rules for Distributions
• 3 An Upper Bound of Robustness from Bayes Error
• 3.1 Certified Training Increases Bayes Error
• 3.2 Irreducible Robustness Error and Robustness Upper Bound
• 4 Experiment and Results
• 5 Related Works
• 6 Conclusion
• References
• Boosting Few-Pixel Robustness Verification via Covering Verification Designs
• 1 Introduction
• 2 Background
• 3 Our Approach: Covering Verification Designs
• 4 CoVerD
• 4.1 Our System
• 4.2 Choosing a Covering Verification Design
• 4.3 Constructing a Covering Verification Design
• 4.4 A Running Example
• 5 Evaluation
• 6 Related Work
• 7 Conclusion
• References
• Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
• 1 Introduction
• 2 Preliminaries
• 2.1 DNN-Controlled Systems
• 2.2 Barrier Certificate and Its Neural Implementation
• 3 Verification Problem and Our Framework
• 3.1 Problem Statement
• 3.2 Overview of Our Framework
• 4 Qualitative and Quantitative Safety Verification.
• 4.1 Qualitative Safety Verification.