Kooperativer Bibliotheksverbund

UID:

Format: 1 Online-Ressource

ISBN: 9783031656330

Series Statement: Lecture notes in computer science 14683

Additional Edition: Erscheint auch als Druck-Ausgabe, Paperback ISBN 978-3-031-65632-3

Language: English

Keywords: Konferenzschrift

DOI: 10.1007/978-3-031-65633-0

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

UID:

Format: 1 online resource (597 pages)

Edition: 1st ed.

ISBN: 9783031656330

Series Statement: Lecture Notes in Computer Science Series ; v.14683

Note: 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 & -- 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.

Additional Edition: Print version: Gurfinkel, Arie Computer Aided Verification Cham : Springer International Publishing AG,c2024 ISBN 9783031656323

Language: English

Keywords: Electronic books.

URL: Click to View

URL: lizenzpflichtig

UID:

Format: 1 online resource (597 pages)

Edition: 1st ed. 2024.

ISBN: 3-031-65633-4

Series Statement: Lecture Notes in Computer Science, 14683

Content: 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 domains such as security, quantum computing, and machine learning.

Note: 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 & -- 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.

Additional Edition: ISBN 3-031-65632-6

Language: English

DOI: 10.1007/978-3-031-65633-0

UID:

Format: 1 online resource (xxv, 582 pages) : , illustrations (chiefly color).

ISBN: 9783031656330 , 3031656334

Series Statement: Lecture notes in computer science, 14683

Content: 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 domains such as security, quantum computing, and machine learning.

Note: International conference proceedings. , Includes author index. , 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 , 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

Language: English

Keywords: Electronic books. ; proceedings (reports) ; Conference papers and proceedings. ; Actes de congrès.

DOI: 10.1007/978-3-031-65633-0

URL: SpringerLink

URL: Click here to view book

UID:

Format: 1 Online-Ressource (597 pages)

Edition: 1st ed. 2024

ISBN: 9783031656330

Series Statement: Lecture Notes in Computer Science 14683

Content: 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 domains such as security, quantum computing, and machine learning

Note: 6 Conclusion and Future Work , 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 & -- 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.

Additional Edition: Erscheint auch als ISBN 3031656326

Language: English

URL: kostenfrei

UID:

Format: XXV, 582 p. 186 illus., 143 illus. in color. , online resource.

Edition: 1st ed. 2024.

ISBN: 9783031656330

Series Statement: Lecture Notes in Computer Science, 14683

Content: 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 domains such as security, quantum computing, and machine learning.

In: Springer Nature eBook

Additional Edition: Printed edition: ISBN 9783031656323

Additional Edition: Printed edition: ISBN 9783031656347

Language: English

DOI: 10.1007/978-3-031-65633-0

URL: https://doi.org/10.1007/978-3-031-65633-0