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, Par

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 II Contents – Part I Tool Demos EVA: a Tool for the Compositional Verification of AUTOSAR Models 1 Introduction 2 A Case Study for Verification in AUTOSAR 3 EVA Verification Workflow 4 Experimental Evaluation 5 Data Availability Statement References WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification 1 Introduction 2 WASIM Functionalities 2.1 Input Processing. 2.2 Representing Simulation States using SMT formulas. 2.3 Symbolic Simulation. 2.4 Expression Simpilification 2.5 Abstraction Refinement. 3 User Interface 3.1 Simulation Process Control. 3.2 Customizable Abstraction/Refinement Function. 3.3 Symbolic State Extraction and Manipulation. 4 Case Studies 5 Related Works 6 Conclusions Data Availability Statement References Multiparty Session Typing in Java, Deductively 1 Introduction 2 Usage: BGJ in a Nutshell 3 Implementation 4 Preliminary Evaluation 5 Conclusion Data Availability Statement References PyLTA: A Verification Tool for Parameterized Distributed Algorithms 1 Introduction 2 Modeling Distributed Algorithms 3 Input Format and Usage 4 Tool Overview and Usage 5 Conclusion References FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format 1 Introduction 2 Word-Level Model Checking and Btor2 Format 3 The FuzzBtor2 Tool 3.1 Usage 3.2 Architecture 4 Experimental Evaluation 5 Conclusion References Eclipse ESCETTM: The Eclipse Supervisory Control Engineering Toolkit 1 Introduction 2 Supervisory Controller Synthesis 3 Synthesis-based Engineering Process 4 Technical Improvements 5 Case Studies and Applications 6 Conclusions 7 Data-Availability Statement References Combinatorial Optimization/Theorem Proving New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization 1 Introduction 2 Preliminaries 3 Core-Guided Algorithm 3.1 Algorithm Description 3.2 Algorithm Properties 4 Hitting Set-based Algorithm 4.1 Algorithm Description 4.2 Algorithm Properties 5 Experimental Results 5.1 Algorithms and Implementation 5.2 Experimental Setup and Benchmark Sets 5.3 Results and Analysis 6 Conclusions Acknowledgements References Verified Reductions for Optimization 1 Introduction 2 Optimization Problems and Reductions 3 Reduction to Conic Form 4 Verifying the Reduction 5 Adding Atoms 6 User-defined Reductions 7 Connecting Lean to a Conic Optimization Solver 8 Related Work 9 Conclusions References Specifying and Verifying Higher-order Rust Iterators 1 Introduction 1.1 Contributions 2 Specifications in Rust Programs 3 Reasoning on Iteration 3.1 Specifying Iterators 3.2 Structural Invariant of for Loops 4 Examples of Specifications of Simple Iterators 4.1 The Range Iterator 4.2 IterMut: Mutating Iteration Over a Vector 4.3 Iterator Adapters 5 Closures in Rust 6 A Higher-order Iterator Adapter: Map 7 Evaluation 8 Related and Future Work Data availability References Extending a High-Performance Prover to Higher-Order Logic 1 Introduction 2 Logic 3 Terms 4 Unification, Matching, and Term Indexing 5 Preprocessing, Calculus, and Extensions 6 Evaluation 7 Discussion and Related Work 8 Conclusion References Tools (Regular Papers) The WhyRel Prototype for Modular Relational Verification of Pointer Programs 1 Introduction 2 A tour of WhyRel 3 Patterns of alignment 4 Encoding and design 5 Evaluation 6 Related work 7 Conclusion Acknowledgments References Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator 1 Introduction 1.1 Our Motivations and Contributions 1.2 Example 2 Related Work 2.1 Compiling Hardware to Software 2.2 Compiling Hardware to Intermediate Representation 3 Background 3.1 The Btor2 Language 3.2 Sequential Circuits and Hardware Model Checking 3.3 Software Model Checking 4 Translating Btor2 to C 4.1 Simulating Sequential Circuits with C Programs 4.2 Variable Naming 4.3 Expressing Btor2 Sorts in C 4.4 Implementing Btor2 Operators in C 4.5 Applying Modulo Operations Lazily 4.6 Discussion 5 Evaluation 5.1 Benchmark Set 5.2 State-of-the-Art Hardware and Software Analysis 5.3 Experimental Setup 5.4 Results 5.5 Discussion 6 Conclusion Acknowledgements. References CoPTIC: Constraint Programming Translated Into C 1 Introduction 2 The Guess-and-Check Paradigm 2.1 Constraint Satisfaction: Magic Square 2.2 CoPTIC Architecture 2.3 Planning: Knight’s Tour 2.4 Enumeration: Integer Quadratics 2.5 Optimisation: Golomb Rulers 3 Practical Considerations 3.1 Debugging Constraint Models 3.2 Performance 4 Evaluation on CSPLib Problems 5 Related Work 6 Conclusion Data Availability Statement References Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability 1 Introduction 2 Preliminaries 3 Realizability algorithm 3.1 Boolean states 3.2 Actions 3.3 Sucient inputs 3.4 Algorithm 4 The many options at every line 4.1 Preprocessing of the automaton (line 1) 4.2 Boolean states (line 2) 4.3 Vectors and downsets (line 3) 4.4 Selecting sucient inputs (line 5) 4.5 Precomputing actions (line 6) 4.6 Main loop: Picking input-actions (line 8) 4.7 When are we done? 5 Checking unrealizability of LTL specfications 6 Benchmarks 6.1 Protocol 6.2 Results 7 Conclusion Acknowledgements. References Synthesis Computing Adequately Permissive Assumptions for Synthesis 1 Introduction 2 Preliminaries 3 Adequately Permissive Assumptions for Synthesis 4 Computing Adequately Permissive Assumptions (APA) 4.1 Preliminaries 4.2 Safety Games 4.3 Live Group Assumptions for Büchi Games 4.4 Co-Liveness Assumptions in Co-Büchi Games 4.5 APA Assumptions for Parity Games 5 Experimental Evaluation 5.1 Performance Evaluation 5.2 2-Client Arbiter Example References Verification-guided Programmatic Controller Synthesis 1 Introduction 2 Problem Setup 3 Programmatic Controllers 4 Proof Space Optimization 4.1 Controller Verification 4.2 Correctness Property Loss in the Proof Space 4.3 Controller Synthesis 5 Experimental Results 6 Related Work 7 Conclusion Acknowledgments References Taming Large Bounds in Synthesis from Bounded-Liveness Specifications 1 Introduction 2 Preliminaries 3 SafeLTLB Synthesis with Countdown-Timer Games 4 Countdown-Timer Game Construction 4.1 Construction of a Countdown-Timer Game from SafeLTLB 5 Solving Countdown-Timer Games 6 Evaluation 7 Conclusion References Lockstep Composition for Unbalanced Loops 1 Introduction 2 Related Work 3 Illustration on Example 4 Preliminaries 4.1 Constrained Horn Clauses 4.2 Relational Verification 5 Equivalence Checking for Unbalanced Loops 5.1 Input Limitations and Auxiliary Definitions 5.2 Equivalence Checking by Decomposition 5.3 Refinement 6 Aligning Unbalanced Loops 6.1 Finding the Number of Iterations 6.2 Identifying Unrolling Depths 6.3 Rearrangement of the Source Projection 7 Evaluation 8 Conclusion References Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification 1 Introduction 2 The Mercury Parameterized Synthesis Problem 2.1 Review: Mercury Systems 2.2 Mercury Process Sketch 2.3 Problem Definition 3 Constraint-Based Synthesis for Mercury Systems 4 Counterexample Extraction 5 Implementation and Evaluation 5.1 Implementation 5.2 Evaluation 6 Related Work References LTL Reactive Synthesis with a Few Hints 1 Introduction 2 Preliminaries on the reactive synthesis problem 3 Synthesis from safety specifications and examples 4 Synthesis from w-regular specifications and examples 5 Implementation and Case study 6 Conclusion References Timed Automata Verification and Synthesis via Finite Automata Learning 1 Introduction 2 Compositional Model Checking 2.1 Preliminaries 2.2 Learning-Based Compositional Model Checking Algorithm 2.3 Experiments 3 Compositional Controller Synthesis 3.1 Preliminaries 3.2 One-Sided Abstraction 3.3 Learning-Based Compositional Controller Synthesis Algorithm 3.4 Experiments 4 Conclusion References Graphs/Probabilistic Systems A Truly Symbolic Linear-Time Algorithm for SCC Decomposition 1 Introduction 1.1 Our Contributions 2 Preliminaries 3 The Chain Algorithm 3.1 Algorithm 3.2 Correctness 3.3 Complexity Analysis 4 Extension to Colored Graphs 4.1 Edge-Colored Graphs 4.2 The ColoredChain Algorithm 5 Experiments 5.1 Experiments on Synthetic Benchmarks 5.2 Experiments on Uncolored Graphs 5.3 Experiments on Colored Graphs 6 Conclusion Acknowledgements. References Transforming Quantified Boolean Formulas Using Biclique Covers 1 Introduction 1.1 Using fewer universal variables 1.2 Overview 2 Preliminaries 2.1 Logic 2.2 Graphs 3 The global conict graph 4 Realisations 4.1 Full clause-sets 4.2 Totally 1-singular clause-sets 4.3 Totally singular MUs 5 A basic generator 6 Experimental results 7 Conclusion and Outlook References Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration 1 Introduction 2 Preliminaries 3 Finding Inductive Upper Bounds in PPS 3.1 Existence of Inductive Upper Bounds 3.2 The Optimistic Value Iteration Algorithm 3.3 Considerations for Implementing OVI 4 Certificates for Probabilistic Pushdown Automata 5 Implementation and Experiments 6 Conclusion and Future Work References Probabilistic Program Verification viaInductive Synthesis of Inductive Invariants 1 Introduction 2 Overview 2.1 Reachability Probabilities and Loops 2.2 Quantitative Inductive Invariants 2.3 Our CEGIS Framework for Synthesizing Inductive Invariants 3 Formal Problem Statement 4 One-Shot Solver 5 Constructing an Ecient CEGIS Loop 5.1 The Verifier 5.2 The Counterexample-Guided Inductive Synthesizer 6 Generalization to Termination and Lower Bounds 7 Empirical Evaluation 8 Related Work References Runtime Monitoring/Program Analysis Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote 1 Introduction 2 The Coyote Tool 3 Coyote Test Engine 3.1 Instrumentation API 3.2 Exploration Strategies 4 Automation for C# Task Asynchronous Programs 4.1 Binary Rewriting for C# Tasks 5 Additional Features 6 Evaluation 7 Related Work References Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis 1 Introduction 2 Data-flow Analysis 3 Meta-analysis for explanations 4 Transforming the box domain 4.1 A naive approach to adding expressions 4.2 A more sophisticated approach to adding expressions 5 Obtaining closed-form expressions 6 Usability and Experimental implementation 7 Generalizability 8 Related work 9 Conclusion Acknowledgments References Explainable Online Monitoring of Metric Temporal Logic 1 Introduction 2 Local Proof System 3 Proof Objects 4 Computing Minimal Proofs 4.1 Monitor’s State 4.2 State Update 4.3 Correctness 5 Implementation 6 Examples 7 Performance 8 Conclusion References 12th Competition on Software Verification — SV-COMP 2023 Competition on Software Verification and Witness Validation: SV-COMP 2023 1 Introduction 2 Organization, Definitions, Formats, and Rules 3 Participating Verifiers and Validators 4 Results of the Verification Track 5 Results of the Witness-Validation Track 6 Conclusion References Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation 1 Witness Validation Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors References 2LS: Arrays and Loop Unwinding 1 Overview 2 Loop Unwinding of Heap-Manipulating Programs 3 Array Domain 4 Strengths andWeaknesses 5 Data-Availablitity Statement References Bubaak: Runtime Monitoring of Program Verifiers 1 Verification Approach 2 Bubaak at SV-COMP 2023 3 Software Architecture 4 Strengths and Weaknesses 5 Results of Bubaak at SV-COMP 2023 References EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs 1 Overview 2 Architecture 3 Strengths andWeaknesses 4 Tool Setup and Configuration 5 Software Project Data-Availability Statement Acknowledgment References Goblint: Autotuning Thread-Modular Abstract Interpretation 1 Verification Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors Bibliography Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution) 1 Introduction 2 Path Merging Extensions and Results 2.1 Run Configuration 2.2 Results 3 Formula Structure in Path-Merged String Constraints 4 Data-Availability Statement References Korn—Software Verification with Horn Clauses (Competition Contribution) 1 Verification Approach 2 Software Architecture 3 Discussion: Strengths and Weaknesses 4 Software Project, Configuration & Participation Data Availability Statement References Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution) 1 Verification Approach: the Mopsa platform 2 Software Architecture: the SV-Comp driver 3 Strengths and Weaknesses 4 Software Project and Contributors References PIChecker: A POR and Interpolation based Verifier for Concurrent Programs(Competition Contribution) 1 Verification Approach 2 Software Architecture 3 Strengths and Weakness 4 Tool Setup and Configuration 5 Software Project and Contributors References Ultimate Automizer and the CommuHash Normal Form (Competition Contribution) 1 Verification Approach 2 SMT formulas in Ultimate 3 The CommuHash Normal Form 4 Project, Setup and Configuration References Ultimate Taipan and Race Detection in Ultimate 1 Verification Approach 2 From Data Races to Reachability 3 Strengths and Weaknesses 4 Architecture, Setup, Configuration , and Project References VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution) 1 Verification Approach 1.1 Strategy Prediction using Machine Learning (ML) 1.2 Shallow Slicer 1.3 Software Project, Architecture, and Setup 2 Data-Availability Statement References VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution) 1 Approach for Non-termination and Termination 1.1 Technique for Non-termination Checking 1.2 Variant of FuzzNT implemented in VeriFuzz 1.4 1.3 Technique for termination 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Configuration and Setup 5 Software Project and Contributors 6 Data-Availability Statement References Author Index