Computer aided cerification : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings. Part I

Computer aided cerification : Part I / 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings. Constantin Enea, Akash Lal, editors.

This open access proceedings set constitutes the refereed proceedings of the 35th International Conference on Computer Aided Verification, CAV 2023, which was held in Paris, France, in July 2023.

Saved in:
Bibliographic Details
Corporate Author: CAV (Conference) Paris, France)
Other Authors: Enea, Constantin (Editor), Lal, Akash (Editor)
Format: eBook
Language:English
Published: Cham, Switzerland : Springer, 2023.
Series:Lecture notes in computer science ; 13964.
Subjects:
Computer software > Verification > Congresses.
Artificial intelligence.
artificial intelligence.
algorithms.
Computer software > Verification
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
Online Access:Click for online access
Table of 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

Similar Items