Cover Image

Tools and Algorithms for the Construction and Analysis of Systems : 29th International Conference, TACAS 2023, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part I.

Bibliographic Details
Main Author: Sankaranarayanan, Sriram.
Other Authors: Sharygina, Natasha.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • ETAPS Foreword
  • Preface
  • Organization
  • Contents - Part I
  • Contents - Part II
  • Invited Talk
  • A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Brief Overview of Martingale Theory
  • 2.2 Problem Statement
  • 3 Supermartingale Certificate Functions
  • 4 Learner-Verifier Framework for Stochastic Systems
  • 4.1 Algorithm Initialization
  • 4.2 The Learner module
  • 4.3 The Verifier module
  • 5 Bounding Expected Values of Neural Networks
  • 6 Discussion on Extension to General Certificates
  • 7 Related Work
  • 8 Conclusion
  • References
  • Model Checking
  • Bounded Model Checking for Asynchronous Hyperproperties
  • 1 Introduction
  • 2 Extended Asynchronous HyperLTL
  • 3 Bounded Model Checking for A-HLTL
  • 3.1 Bounded Semantics of A-HLTL
  • 3.2 From Bounded Semantics to QBF Solving
  • 4 Complexity of A-HLTL Model Checking for AcyclicFrames
  • 5 Case Studies and Evaluation
  • 5.1 Analysis of Experimental Results
  • 6 Conclusion and Future Work
  • References
  • Model Checking Linear Dynamical Systems under Floating-point Rounding
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Linear dynamical systems and rounding functions
  • 2.2 Model checking
  • 2.3 Structure of M
  • 3 Undecidability of point-to-point reachability
  • 4 Pseudo-periodic orbits of non-negative LDS
  • 4.1 Preprocessing periodicity
  • 4.2 Pseudo-periodicity within top SCCs
  • 4.3 Pseudo-periodicity within lower SCCs
  • 5 Decidability of model checking
  • Acknowledgements
  • References
  • Efficient Loop Conditions for Bounded Model Checking Hyperproperties
  • 1 Introduction
  • 2 Preliminaries
  • 3 Adaptation of BMC to HyperLTL on Infinite Traces
  • 4 Simulation-Based BMC Algorithms for HyperLTL
  • 4.1 Encodings for EA-Simulation
  • 4.2 Encodings for AE-Simulation.
  • 4.3 Encodings for AE-Simulation with Prophecies
  • 5 Implementation and Experiments
  • 5.1 Case Studies and Empirical Evaluation
  • 5.2 Analysis and Discussion
  • 6 Conclusion and Future Work
  • References
  • Reconciling Preemption Bounding with DPOR
  • 1 Introduction
  • 2 Background
  • 2.1 The Basics of Dynamic Partial Order Reduction
  • 2.2 Bounded Partial Order Reduction
  • 2.3 TruSt: Optimal Dynamic Partial Order Reduction
  • 3 Bounded Optimal DPOR: Obstacles
  • 3.1 Pessimistic Bound Definition
  • 3.2 Need For Slack
  • 4 Recovering Completeness via Slack
  • 4.1 Properties of TruSt
  • 4.2 Correctness of Slacked Bounding
  • 5 Implementation
  • 6 Evaluation
  • 6.1 Bound and Bug Manifestation
  • 6.2 Comparison with Plain DPOR on Safe Benchmarks
  • 6.3 Bound Calculation Overhead
  • 6.4 Overhead due to Bound-Blocked Executions
  • 7 Related Work
  • Acknowledgments
  • 8 Data-Availability Statement
  • References
  • Optimal Stateless Model Checking for Causal Consistency
  • 1 Introduction
  • 2 Preliminaries
  • 3 Causally Consistent Models
  • 4 Trace Semantics
  • 5 DPOR Algorithm for CC, CCv, CM
  • 6 Experimental Evaluation
  • 6.1 Litmus Benchmarks
  • 6.2 SV-COMP Benchmarks
  • 6.3 Database Applications
  • 6.4 Classical Benchmarks
  • 6.5 Parameterized Benchmarks
  • 7 Conclusion
  • 8 Data-Availability Statement
  • References
  • Symbolic Model Checking for TLA+ Made Faster
  • 1 Introduction
  • 2 Background
  • 2.1 TLA+
  • 2.2 KerA+
  • 2.3 Abstract Reduction System
  • 2.4 SMT Theory of Arrays
  • 3 Encoding TLA+ using Arrays
  • 3.1 Encoding TLA+ Sets using Arrays
  • 3.2 Encoding TLA+ Functions using Arrays
  • 3.3 Correctness of the Reduction to Arrays
  • 4 Evaluation
  • 4.1 Benchmarks
  • 4.2 Results
  • 5 Related Work
  • 6 Conclusions
  • Acknowledgements
  • References
  • AutoHyper: Explicit-State Model Checking for HyperLTL
  • 1 Introduction
  • 2 Preliminaries.
  • 3 Automata-based HyperLTL Model Checking
  • 3.1 Automata-based Verification
  • 3.2 HyperLTL Model Checking by Language Inclusion
  • 4 Related Work and HyperLTL Verification Approaches
  • 5 AutoHyper: Tool Overview
  • 6 HyperLTL Model Checking Complexity in Practice
  • 6.1 Performance of Inclusion Checkers
  • 6.2 Model Checking Beyond ∀∗∃∗
  • 7 Evaluation on Symbolic Systems
  • 7.1 Model Checking GNI on Boolean Programs
  • 7.2 Explicit Model Checking of Symbolic Systems
  • 7.3 Hyperproperties for Path Planning
  • 7.4 Bounded vs. Explicit-State Model Checking
  • 8 Evaluating Strategy-based Verification
  • 8.1 Effectiveness of Strategy-based Verification
  • 8.2 Efficiency of Strategy-based Verification
  • 9 Conclusion
  • Acknowledgments
  • Data Availability Statement
  • References
  • Machine Learning/Neural Networks
  • Feature Necessity &amp
  • Relevancyin ML Classifier Explanations
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Classification Problems
  • 2.2 Examples of Classifiers
  • 2.3 Formal Explainability
  • 3 Feature Relevancy &amp
  • Necessity: Theory
  • 3.1 Defining Necessity, Relevancy &amp
  • Irrelevancy
  • 3.2 Feature Necessity
  • 3.3 Feature Relevancy: Membership Results
  • 3.4 Feature Relevancy: Hardness Results
  • 4 Feature Relevancy: Example Algorithms
  • 4.1 Relevancy for d-DNNF Classifiers
  • 4.2 Relevancy for Monotonic Classifiers
  • 5 Experimental Results
  • 6 Related Work
  • 7 Conclusions
  • Acknowledgements
  • References
  • Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
  • 1 Introduction
  • 2 Background
  • 3 Provable Approximations for Minimal Explanations
  • 4 Finding Minimal Explanations Efficiently
  • 5 Minimal Bundle Explanations
  • 6 Evaluation
  • 7 Related Work
  • 8 Conclusion
  • References
  • OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
  • 1 Introduction.
  • 2 Preliminaries
  • 2.1 Deep Neural Networks and the Robustness
  • 2.2 Occlusion Perturbation
  • 3 The Occlusion Robustness Verification Problem
  • 4 SMT-Based Occlusion Robustness Verification
  • 4.1 A Naïve SMT Encoding Method
  • 4.2 Our Encoding Approach
  • 4.3 The Correctness of the Encoding
  • 4.4 Verification Acceleration Techniques
  • 5 Implementation and Evaluation
  • 6 Related Work
  • 7 Conclusion and Future Work
  • Acknowledgments
  • References
  • Neural Network-Guided Synthesis of Recursive List Functions
  • 1 Introduction
  • 2 The Synthesis Problem
  • 3 The Design and Training of the RNN
  • 3.1 The Architecture of the RNN
  • 3.2 Training the RNN
  • 4 Synthesis Based on the Trained RNN
  • 5 Implementation and Experiments
  • 5.1 Dataset and predicates
  • 5.2 Evaluation
  • 6 Related Work
  • 7 Conclusion
  • Acknowledgments
  • References
  • Automata
  • Modular Mix-and-Match Complementation of Buchi Automata
  • 1 Introduction
  • 2 Preliminaries
  • 3 A Modular Complementation Algorithm
  • 3.1 Basic Synchronous Algorithm
  • 4 Modular Complementation of Elevator Automata
  • 4.1 Complementation of Inherently Weak Accepting Components
  • 4.2 Complementation of Deterministic Accepting Components
  • 4.3 Upper-bound for Elevator Automata Complementation
  • 5 Optimizations of the Modular Construction
  • 5.1 Complementation of Initial Deterministic Partition Blocks
  • 5.2 Postponed Construction
  • 5.3 Round-Robin Algorithm
  • 5.4 Shared Breakpoint
  • 5.5 Simulation Pruning
  • 6 Modular Complementation of Non-Elevator Automata
  • 7 Experimental Evaluation
  • 8 Related Work
  • 9 Conclusion and Future Work
  • References
  • Validating Streaming JSON Documents with Learned VPAs
  • 1 Introduction
  • 2 Visibly Pushdown Languages
  • 3 JSON Format
  • 4 Validation of JSON Documents
  • 5 Implementation and Experiments
  • 6 Future Work
  • References.
  • Antichains Algorithms for the Inclusion Problem Between ω-VPL
  • 1 Introduction
  • 2 Background
  • 3 Foundations
  • 4 Fixpoint Characterization
  • 5 Monotonicity Requirements
  • 6 Quasiorders for ω-VPL
  • 7 Algorithm
  • 7.1 State-based Algorithm
  • 8 Experiments
  • 9 Conclusion and Future Work
  • References
  • Stack-Aware Hyperproperties
  • 1 Introduction
  • 2 Motivation
  • 3 Stack-aware Hyper Computation Tree Logic (sHCTL*)
  • 3.1 Pushdown Systems
  • 3.2 Syntax of sHCTL*
  • 3.3 Semantics of sHCTL*
  • 4 A Decision Procedure for sHCTL*
  • 4.1 Automata on Pushdown Alphabets
  • 4.2 Algorithm for sHCTL*
  • 5 Lower Bound
  • 6 Conclusions
  • References
  • Proofs
  • Propositional Proof Skeletons
  • 1 Introduction
  • 2 Background and Related Work
  • 3 Problem Overview
  • 4 Creating Proof Skeletons
  • 4.1 Online Generation of Proof Skeletons
  • 4.2 Offline Generation of Proof Skeletons
  • 5 Reconstructing Proofs from Skeletons
  • 5.1 Filling Skeletons Using Incremental Solvers
  • 5.2 Shrinking Skeletons
  • 5.3 Reconstructing LRAT Proofs from Skeletons
  • 6 Experimental Evaluation
  • 6.1 Single-Core Proof Reconstruction
  • 6.2 Skeleton Compression Ratio
  • 6.3 Impact of Reason Clauses in Online Skeletons
  • 6.4 Impact of the UNSAT Core on Offline Skeletons
  • 6.5 Skeleton Shrinking after Reconstruction
  • 6.6 Comparison With Sequential and Parallel SAT Solvers
  • 7 Conclusion
  • References
  • Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
  • 1 Introduction
  • 2 Background and Related Work
  • 3 Basic Proof Production
  • 3.1 Solver Partial Proof Production
  • 3.2 Partial Proof Combination
  • 3.3 Proof Pruning
  • 4 Distributed Proof Production
  • 4.1 Overview
  • 4.2 Distributed Pruning
  • 4.3 Merging Step
  • 5 Implementation
  • 6 Evaluation
  • 6.1 Experimental Setup
  • 6.2 Results
  • 7 Conclusion and Future Work
  • Acknowledgments.
  • References.

Similar Items