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 2022 Paris, France, April 22–27, 2023 Proceedings, Part I

Description

This open access book constitutes the proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, during April 22-27, 2023, in Paris, France. The 56 full papers and 6 short tool demonstration papers presented in this volume were carefully reviewed and selected from 169 submissions. The proceedings also contain 1 invited talk in full paper length, 13 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report. TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility, and efficiency of tools and algorithms for building computer-controlled systems.   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 & Relevancyin ML Classifier Explanations 1 Introduction 2 Preliminaries 2.1 Classification Problems 2.2 Examples of Classifiers 2.3 Formal Explainability 3 Feature Relevancy & Necessity: Theory 3.1 Defining Necessity, Relevancy & 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 CARCARA: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format⋆ 1 Introduction 1.1 Related work 2 The Alethe Proof Format 3 Architecture and core components 3.1 Checking Alethe proofs 3.2 Elaborating Alethe proofs 4 Evaluation 4.1 Proof checking 4.2 Proof elaboration References Constraint Solving/Blockchain The Packing Chromatic Number of the Infinite Square Grid is 15 1 Introduction 2 Background 3 Optimizations 3.1 “Plus”: a New Encoding 3.2 Symmetry Breaking 3.3 At-Least-One-Distance clauses 3.4 Cube And Conquer Using Auxiliary Variables 3.5 Optimizing the Center Color 4 Verification 5 Experiments 6 Concluding Remarks and Future Work Acknowledgements References Active Learning for SAT Solver Benchmarking 1 Introduction 2 Related Work 3 Active Learning for SAT Solver Benchmarking 3.1 Solver Model 3.2 Instance Selection 3.3 Stopping Criteria 4 Experimental Design 4.1 Evaluation Framework 4.2 Data 4.3 Hyper-parameters 4.4 Implementation Details 5 Evaluation 5.1 Hyper-Parameter Analysis 5.2 Full-Dataset Evaluation 5.3 Instance-Family Importance 6 Conclusions and Future Work References ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving⋆ 1 Introduction 2 Preliminaries 3 Related Work 4 ParaCooba 5 Architecture of ParaQooba: Combining Divide-and-Conquer Portfolio Solving 6 Implementation 6.1 The ParaQooba QBF Module 6.2 Search-Space Pruning 7 Evaluation 7.1 Overall Performance Comparison 7.2 Family-Based Analysis 7.3 Scalability of our Approach 7.4 Preprocessed Leaves compared to Preprocessed Formulas 7.5 Lessons Learned 8 Conclusions References Inferring Needless Write Memory Accesses on Ethereum Bytecode? 1 Introduction 2 Memory Layout and Motivating Examples 3 Inference of Needless Write Accesses 3.1 Context-Sensitive CFG and Flow-Sensitive Static Analysis 3.2 Slot Analysis 3.3 Slot Access Analysis 3.4 Inference of Needless Write Memory Accesses 4 Experimental Evaluation 5 Conclusions and Related Work References Markov Chains/Stochastic Control A Practitioner’s Guide to MDP Model Checking Algorithms 1 Introduction 2 Background 2.1 Markov Decision Processes 2.2 Solution Algorithms 2.3 Guarantees 2.4 Optimizations 3 Practically solving MDPs using Linear Programs 3.1 How to encode MDPs as LPs? 3.2 How to solve LPs with existing solvers? 4 Sound Policy Iteration 5 Experimental Evaluation 5.1 The QVBS Benchmarks 5.2 The Hard QVBS Benchmarks 5.3 The Runtime Monitoring Benchmarks 6 Conclusion References Correct Approximation of Stationary Distributions 1 Introduction 1.1 Contributions 1.2 Related Work 2 Preliminaries 3 Building Blocks 3.1 Bounds in BSSCs through Mean Payoff 3.2 Reachability and Guided Sampling 4 Dynamic Computation with Partial Exploration 4.1 The Framework 4.2 Sampling-Based Computation 5 Experimental Evaluation 6 Conclusion References Robust Almost-Sure Reachability in Multi-Environment MDPs 1 Introduction 2 Problem Statement 3 A Reduction To Belief-Observation MDPs 3.1 Interpretation of MEMDPs as Partially Observable MDPs 3.2 Belief-observation MDPs 3.3 Fragments of BOMDPs 4 Computational Complexity 4.1 Deciding Almost-Sure Winning for MEMDPs in PSPACE 4.2 Deciding Almost-Sure Winning for MEMDPs Is PSPACE-hard 4.3 Policy Problem 5 A Partial Game Exploration Algorithm 6 Experiments 7 Conclusion References Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning 1 Introduction 2 Overview of Mungojerrie 3 Tool Design 4 Case Studies 4.1 Comparing Reward Schemes 4.2 Comparing Automata 4.3 A Game of Pursuit 5 Conclusion References Verification A Formal CHERI-C Semantics for Verification 1 Introduction 2 CHERI 3 CHERI-C Memory Model 3.1 Design 3.2 Type and Value System 3.3 Memory 3.4 Operations 3.5 Properties 4 Application 4.1 Isabelle/HOL 4.2 Gillian 4.3 Compiler 5 Experimental Results 6 Related Work 7 Conclusion and Future Work Acknowledgements References Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm 1 Introduction 2 Overview 2.1 . TimEffs 2.2 . Forward Verification 2.3 . The TRS 2.4 . Verifying the Fischer’s Mutual Exclusion Protocol 3 Language and Specifications 3.1 The Target Language 3.2 Operational Semantics of Ct 3.3 The Specification Language 3.4 Semantic Model of Timed Effects 4 Automated Forward Verification 4.1 Forward Rules 5 Temporal Verification via a TRS 5.1 Rewriting Rules 6 Implementation and Evaluation 6.1 . Experimental Results for Symbolic Timed Models. 6.2 . Verifying Fischer's mutual exclusion algorithm 6.3 . Case Study: Prove it when Reoccur 6.4 . Discussion 7 Related Work 7.1 . Verification Framework 7.2 . Specifications and Real-Time Verification 7.3 . Clock Manipulation and Zone-based Bisimulation 8 Conclusion 9 Acknowledgements References Parameterized Verification under TSO with Data Types 1 Introduction 2 Preliminaries 3 Abstract Data Types (ADT) 4 TSO with an Abstract Data Type : TSO(A) 5 Parameterized Reachability in TSO(A) 6 Register Machines 6.1 Simulating Pivot Abstraction by Register Machines 6.2 Simulating Register Machines by TSO 7 Instantiations of ADTs 8 Conclusions and Future Work References Verifying Learning-Based Robotic Navigation Systems 1 Introduction 2 Background 3 Case Study: Robotic Mapless Navigation 4 Using Verification for Model Selection 5 Experimental Evaluation 6 Related Work 7 Conclusion References Make Flows Small Again: Revisiting the Flow Framework 1 Introduction 2 Flow Graph Separation Algebra 3 Frame-Preserving Updates 4 Computing Footprints 4.1 Algorithm 4.2 Comparing Transfer Functions 5 Evaluation 6 Related Work References ALASCA: Reasoning in Quantified Linear Arithmetic 1 Introduction 2 Motivating Example 3 Background and Notation 4 Theoretical Foundation for Unification with Abstraction 4.1 Unification with Abstraction – UWA 4.2 UWA Completeness 5 ALASCA Reasoning 5.1 The ALASCA Calculus – Ground Version 5.2 ALASCA Lifting and Completeness 6 Implementation and Experiments 7 Conclusions and Future Work References A Matrix-Based Approach to Parity Games 1 Introduction 2 Preliminaries 3 A matrix-based approach 3.1 Complexity 4 Implementation and evaluation 4.1 Evaluation 5 Analysis of results 6 Special cases 6.1 Solving large parity games 6.2 Solving random parity games 7 Alternative implementations 8 Concluding remarks and related work References A GPU Tree Database for Many-Core Explicit State Space Exploration 1 Introduction 2 Related Work 3 GPU programming 4 GPU state space exploration 5 A Compact GPU Tree Database 5.1 CPU Tree Storage 5.2 GPU Tree Generation 5.3 GPU Tree Storage at Block Level 5.4 Single Node Storage at Bucket Group Level 6 Experiments 7 Conclusions and Future Work References Author Index