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.