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.