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.

• Superior document: Lecture Notes in Computer Science Series ; v.13993
• Author: Sankaranarayanan, Sriram.
• TeilnehmendeR: Sharygina, Natasha.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2023.; ©2023.
• Year of Publication: 2023
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (718 pages)

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.