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

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