Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24–27, 2024, Proceedings, Part II / edited by Arie Gurfinkel, Vijay Ganesh.

Format:

Book

Author/Creator:

Gurfinkel, Arie.

Contributor:

Ganesh, Vijay.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 14682

Language:

English

Subjects (All):

Software engineering.

Artificial intelligence.

Algorithms.

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Local Subjects:

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Physical Description:

1 online resource (447 pages)

Edition:

1st ed. 2024.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2024.

Summary:

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.

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

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

Collective Contracts for Message-Passing Parallel Programs

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

Distributed Systems

mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic

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

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas

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.1 Implementation

6.2 Experiments

6.3 Results

Verifying Cake-Cutting, Faster

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

7 Related and Future Work

Runtime Verification and Monitoring

General Anticipatory Runtime Verification

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

Proactive Real-Time First-Order Enforcement

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

Predictive Monitoring with Strong Trace Prefixes

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

Case Studies and Tools

Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned

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

Testing the Migration from Analog to Software-Based Railway Interlocking Systems

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

soid: A Tool for Legal Accountability for Automated Decision Making

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

Machine Learning and Neural Networks

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

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

Monitizer: Automating Design and Evaluation of Neural Network Monitors

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

Guiding Enumerative Program Synthesis with Large Language Models

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

Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification

2 Background and Motivation

3 Methodology

3.1 Code Decomposition

3.2 Hierarchical Specification Generation

3.3 Specification Validation

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

Verifying Global Two-Safety Properties in Neural Networks with Confidence

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.1 Discussion

Certified Robust Accuracy of Neural Networks Are Bounded Due to Bayes Errors

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

Boosting Few-Pixel Robustness Verification via Covering Verification Designs

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

Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems

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.

ISBN:

3-031-65630-X