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

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

This open access book constitutes the proceedings of the 36th International Conference on Computer-Aided Verification, CAV 2024, which took place in Montreal, Canada, during July 24–27, 2024.

Detalles Bibliográficos
Autor principal: Gurfinkel, Arie (-)
Otros Autores: Ganesh, Vijay
Formato: Libro electrónico
Idioma:Inglés
Publicado: Cham : Springer Nature Switzerland 2024.
Edición:1st ed. 2024.
Colección:Lecture Notes in Computer Science, 14682
Materias:
Software engineering.
Artificial intelligence.
Algorithms.
Software Engineering.
Artificial Intelligence.
Design and Analysis of Algorithms.
Ver en Biblioteca Universitat Ramon Llull:https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009845838006719
Tabla de Contenidos:
  • 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.

Ejemplares similares