Computer Aided Verification : : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.13964 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer,, 2023. ©2023. |
Year of Publication: | 2023 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (512 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
50030651887 |
---|---|
ctrlnum |
(MiAaPQ)50030651887 (Au-PeEL)EBL30651887 (OCoLC)1390710955 |
collection |
bib_alma |
record_format |
marc |
spelling |
Enea, Constantin. Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. 1st ed. Cham : Springer, 2023. ©2023. 1 online resource (512 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.13964 Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods. 4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity. 3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples. 8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References. Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification. 7 Implementation and Experiments. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. Lal, Akash. Print version: Enea, Constantin Computer Aided Verification Cham : Springer,c2023 9783031377051 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=30651887 Click to View |
language |
English |
format |
eBook |
author |
Enea, Constantin. |
spellingShingle |
Enea, Constantin. Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. Lecture Notes in Computer Science Series ; Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods. 4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity. 3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples. 8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References. Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification. 7 Implementation and Experiments. |
author_facet |
Enea, Constantin. Lal, Akash. |
author_variant |
c e ce |
author2 |
Lal, Akash. |
author2_variant |
a l al |
author2_role |
TeilnehmendeR |
author_sort |
Enea, Constantin. |
title |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_sub |
35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_full |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_fullStr |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_full_unstemmed |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_auth |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
title_new |
Computer Aided Verification : |
title_sort |
computer aided verification : 35th international conference, cav 2023, paris, france, july 17-22, 2023, proceedings, part i. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer, |
publishDate |
2023 |
physical |
1 online resource (512 pages) |
edition |
1st ed. |
contents |
Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods. 4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity. 3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples. 8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References. Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification. 7 Implementation and Experiments. |
isbn |
9783031377068 9783031377051 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.758 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=30651887 |
illustrated |
Not Illustrated |
oclc_num |
1390710955 |
work_keys_str_mv |
AT eneaconstantin computeraidedverification35thinternationalconferencecav2023parisfrancejuly17222023proceedingsparti AT lalakash computeraidedverification35thinternationalconferencecav2023parisfrancejuly17222023proceedingsparti |
status_str |
n |
ids_txt_mv |
(MiAaPQ)50030651887 (Au-PeEL)EBL30651887 (OCoLC)1390710955 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.13964 |
is_hierarchy_title |
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. |
container_title |
Lecture Notes in Computer Science Series ; v.13964 |
author2_original_writing_str_mv |
noLinkedField |
marc_error |
Info : MARC8 translation shorter than ISO-8859-1, choosing MARC8. --- [ 856 : z ] |
_version_ |
1792331071230050304 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11053nam a22004693i 4500</leader><controlfield tag="001">50030651887</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073851.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2023 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783031377068</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783031377051</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)50030651887</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL30651887</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1390710955</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.758</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Enea, Constantin.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer Aided Verification :</subfield><subfield code="b">35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer,</subfield><subfield code="c">2023.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2023.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (512 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.13964</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">7 Implementation and Experiments.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="a">Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Lal, Akash.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Enea, Constantin</subfield><subfield code="t">Computer Aided Verification</subfield><subfield code="d">Cham : Springer,c2023</subfield><subfield code="z">9783031377051</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=30651887</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |