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.