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

• Superior document: Lecture Notes in Computer Science Series ; v.14683
• 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 (597 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 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.