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

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

This open access 3-volume set 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. The primary focus of CAV is to extend the frontiers of verification techniques by expanding to new d...

Full description

Bibliographic Details
Main Author: Gurfinkel, Arie (-)
Other Authors: Ganesh, Vijay
Format: eBook
Language:Inglés
Published: Cham : Springer Nature Switzerland 2024.
Edition:1st ed. 2024.
Series:Lecture Notes in Computer Science, 14683
Subjects:
Software engineering.
Artificial intelligence.
Algorithms.
Software Engineering.
Artificial Intelligence.
Design and Analysis of Algorithms.
See on Biblioteca Universitat Ramon Llull:https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009845838406719
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 III
  • Synthesis and Repair
  • Syntax-Guided Automated Program Repair for Hyperproperties
  • 1 Introduction
  • 2 Preliminaries
  • 3 Program Repair by Symbolic Execution
  • 3.1 Symbolic Execution
  • 3.2 Symbolic Paths and Safety Automata
  • 3.3 Encoding for HyperLTL
  • 3.4 Program Repair Using SyGuS
  • 4 Transparent Repair
  • 4.1 Transparency
  • 4.2 Encoding for Transparent Repair
  • 5 Iterative Repair
  • 5.1 Encoding for Iterative Repair
  • 5.2 Iterative Repair Loop
  • 6 Implementation and Evaluation
  • 6.1 Iterative Repair for Hyperproperties
  • 6.2 Scalability in Solution Size
  • 6.3 Evaluation on k-Safety Instances
  • 6.4 Evaluation on Functional Properties
  • 7 Related Work
  • 8 Conclusion
  • References
  • The SemGuS Toolkit
  • 1 Introduction
  • 2 The SemGuS Format 1.0
  • 3 A Baseline SemGuS Solver
  • 3.1 Verifying Candidate Solutions
  • 3.2 Baseline Enumerative Solvers
  • 3.3 Extensibility
  • 4 Benchmarks and Performance of Baseline Solvers
  • 5 Related Work
  • References
  • Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata
  • 1 Introduction
  • 2 Motivating Example
  • 3 Preliminaries
  • 4 Constraint Annotated Tree Automata
  • 4.1 CATA Operations for Synthesis
  • 5 Synthesis Algorithm
  • 5.1 Problem Statement
  • 5.2 Basic Synthesis Algorithm
  • 5.3 Lazy Synthesis Algorithm
  • 6 Implementation
  • 7 Evaluation
  • 8 Related Work
  • 9 Conclusion
  • References
  • Information Flow Guided Synthesis with Unbounded Communication
  • 1 Introduction
  • 2 Running Example: Sequence Transmission
  • 3 Preliminaries
  • 4 Prefix Information Flow
  • 5 Unbounded Communication in Distributed Systems
  • 5.1 Receiving Information.
  • 5.2 Transmitting Information
  • 5.3 Safety Hyper Implementations
  • 6 Synthesis with Prefix Information Flow Assumptions
  • 6.1 Automata for Assume and Guarantee Specifications
  • 6.2 Compositional Synthesis
  • 7 Experiments
  • 8 Related Work
  • 9 Conclusion
  • References
  • Synthesis of Temporal Causality
  • 1 Introduction
  • 1.1 Temporal Causality
  • 1.2 Contributions and Structure
  • 2 Preliminaries
  • 3 Overview: The Topology of Causality
  • 3.1 Actual Causes as Downward Closed Sets of Traces
  • 3.2 Causality Without the Limit Assumption
  • 4 Generalized Temporal Causality
  • 4.1 Similarity Relations and the Limit Assumption
  • 4.2 A General Definition of Temporal Causality
  • 4.3 Proving Generalization
  • 5 Cause Synthesis
  • 5.1 Proving Our Characterization
  • 5.2 Cause-Synthesis Algorithm for -Regular Effects
  • 6 Implementation and Evaluation
  • 6.1 Cause Synthesis
  • 6.2 Cause Checking
  • 7 Related Work
  • 8 Conclusion
  • References
  • Dynamic Programming for Symbolic Boolean Realizability and Synthesis
  • 1 Introduction
  • 2 Preliminary Definitions
  • 2.1 Boolean Formula and Synthesis Concepts
  • 2.2 Dynamic Programming Concepts - Project-Join Trees
  • 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A.
  • 3.1 Theoretical Basis and Valuations in Trees
  • 3.2 Determining Nullary, Partial and Full Realizability
  • 4 Synthesis of Witness Functions
  • 4.1 Monolithic Approach
  • 4.2 Synthesis Using Graded Project-Join Trees
  • 5 Experimental Evaluation
  • 5.1 Realizability-Checking Phase
  • 5.2 Synthesis
  • 5.3 Tree Widths and Realizability
  • 5.4 Comparison with Non-BDD-Based Synthesis
  • 6 Concluding Remarks
  • References
  • Localized Attractor Computations for Infinite-State Games
  • 1 Introduction
  • 2 Preliminaries
  • 3 Attractor Computation with Caching
  • 4 Abstract Template-Based Cache Generation.
  • 4.1 Generating Attractor Caches from Sub-Games
  • 4.2 Constructing Sub-games from Abstract Strategy Templates
  • 5 Game Solving with Abstract Template-Based Caching
  • 6 Experimental Evaluation
  • 7 Related Work
  • 8 Conclusion
  • References
  • Learning
  • Bisimulation Learning
  • 1 Introduction
  • 2 Illustrative Example
  • 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems
  • 3.1 Model Checking
  • 4 Counterexample-Guided Bisimulation Learning
  • 4.1 Learner-Verifier Framework for Bisimulation Learning
  • 4.2 Binary Decision Tree Partition Templates
  • 5 Experimental Evaluation
  • 5.1 Discrete-Time Clock Synchronization
  • 5.2 Conditional Termination
  • 6 Conclusion
  • References
  • Regular Reinforcement Learning
  • 1 Introduction
  • 2 Related Work
  • 3 Preliminaries
  • 3.1 Regular Languages
  • 3.2 Rational Transductions
  • 3.3 Markov Decision Processes
  • 4 Regular Markov Decision Processes
  • 4.1 Undecidability of Values
  • 4.2 Discounted Optimization
  • 4.3 Finiteness Conditions
  • 4.4 Q-Learning in RMDPs
  • 5 Deep Regular Reinforcement Learning
  • 5.1 Token Passing
  • 5.2 Duplicating Pebbles
  • 5.3 Shunting Yard Algorithm
  • 5.4 Modified Tangrams
  • 6 Conclusion
  • References
  • LTL Learning on GPUs
  • 1 Introduction
  • 2 Formal Preliminaries
  • 3 High-Level Structure of the Algorithm
  • 4 In-Memory Representation of Search Space
  • 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators
  • 6 Relaxed Uniqueness Checks
  • 7 Divide &amp
  • Conquer
  • 8 Evaluation of Algorithm Performance
  • 9 Conclusion
  • References
  • Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
  • 1 Introduction
  • 2 Problem Setup
  • 3 Verified Exploration Through Learned Models
  • 3.1 Symbolic Environment Models
  • 3.2 Shielding for Verified Safe Exploration.
  • 3.3 Neural Controller Approximation
  • 4 Experiments
  • 5 Related Work
  • 6 Conclusion
  • References
  • Cyberphysical and Hybrid Systems
  • Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
  • 1 Introduction
  • 1.1 Related Work
  • 1.2 Contributions
  • 2 Preliminaries and Problem Statement
  • 2.1 Intervals
  • 2.2 Truth Values
  • 2.3 Signals
  • 2.4 Reachability Analysis of Hybrid Systems
  • 2.5 Signal Temporal Logic with Boolean Semantics
  • 2.6 Problem Statement
  • 3 Basic Idea and Solution Concept
  • 4 Four-Valued Signal Temporal Logic
  • 4.1 Computing Boolean Satisfaction Signals
  • 4.2 Computing Three-Valued Satisfaction Signals
  • 4.3 Computing Four-Valued Satisfaction Signals
  • 5 Incremental Verification of Hybrid Systems
  • 5.1 Incremental Verification Algorithm
  • 5.2 Refinement via Branching the Reachability Analysis
  • 6 Evaluation
  • 6.1 Bouncing Ball
  • 6.2 Autonomous Driving
  • 6.3 Genetic Oscillator
  • 7 Conclusion
  • References
  • Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Signal Temporal Logic
  • 2.2 Finite Variability
  • 3 Problem Formulation
  • 4 Variable-Interval Encoding of STL to MILP
  • 4.1 -Stable Partitions
  • 4.2 Variable-Interval MILP Encoding
  • 5 System Models and Their MILP Encoding
  • 5.1 HAs with Closed-Form Solutions
  • 5.2 HAs with Double Integrator Dynamics
  • 6 Implementation and Experiments
  • References
  • Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Notation
  • 2.2 Problem Statement
  • 3 Methodology
  • 3.1 Inner-Approximation Computation Framework
  • 3.2 Extraction of Zonotopes' Boundaries
  • 3.3 Zonotopal Tiling and Boundary Refinement
  • 3.4 Contracting Computed Outer-Approximation
  • 4 Experiments.
  • 4.1 Advantage in Efficiency and Precision
  • 4.2 Advantage in Long Time Horizons
  • 4.3 Advantage in Big Initial Sets
  • 5 Conclusion
  • References
  • Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
  • 1 Introduction
  • 2 Background
  • 2.1 Preliminaries
  • 2.2 Motivating Example: A Multi-UAV System
  • 3 Scenario-Based Formalism for Reconfigurable Systems
  • 3.1 Scenario-Based System Modeling
  • 3.2 Specifying System Requirements in Topology-Aware STL
  • 4 Path-Oriented Optimization-Based System Falsification
  • 4.1 Falsification Framework
  • 4.2 Path Generation for Hierarchical Scenario Tasks
  • 4.3 Optimization-Based Falsification for Paths
  • 5 Implementation and Evaluation
  • 5.1 Implementation and Research Questions
  • 5.2 Experimental Evaluation and Analysis
  • 5.3 Threats to Validity
  • 6 Related Work
  • 7 Conclusion and Future Work
  • References
  • Probabilistic Systems
  • Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games
  • 1 Introduction
  • 2 Preliminaries
  • 3 Complete-Exploration Algorithm for Solving SGs
  • 4 Partial-Exploration Algorithm for Solving SGs
  • 5 Tool Description
  • 6 Experimental Evaluation
  • 6.1 Experimental Setup
  • 6.2 Results
  • 7 Conclusion
  • References
  • What Should Be Observed for Optimal Reward in POMDPs?
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Markov Decision Processes (MDPs)
  • 2.2 Partially Observable Markov Decision Processes
  • 3 The Optimal Observability Problem
  • 3.1 Problem Statement
  • 3.2 Undecidability
  • 4 Optimal Observability for Positional Strategies
  • 4.1 Positional and Deterministic Strategies
  • 4.2 Positional Randomized Strategies
  • 5 Implementation and Experimental Evaluation
  • 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools
  • 5.2 Implementation and Setup
  • 5.3 Experimental Results.
  • 6 Conclusion and Future Work.

Similar Items