Model Checking Software : 29th International Symposium, SPIN 2023, Paris, France, April 26–27, 2023, Proceedings

This book constitutes the refereed proceedings of the 29th International Symposium on Model Checking Software, SPIN 2023, held in Paris, France, during April 26–27, 2023. The 9 full papers and 2 short papers included in this book were carefully reviewed and selected from 21 submissions. They were organized in topical sections as follows: binary decision diagrams, concurrency, testing, synthesis, explicit-state model checking. Preface 6 Organization 7 Contents 9 Binary Decision Diagrams 11 Efficient Implementation of LIMDDs for Quantum Circuit Simulation 12 1 Introduction 12 2 Background 14 2.1 Quantum States and Operations 15 2.2 Classical Quantum Circuit Simulation 17 2.3 Verification of Quantum Circuits 18 3 Motivation 18 3.1 Quantum Multiple-valued Decision Diagrams (QMDDs) 19 3.2 Local Invertible Map Decision Diagrams (LIMDDs) 21 3.3 The Need for a LIMDD Implementation 21 4 Implementation of LIMDDs 22 4.1 Established Techniques 22 4.2 Implementing Local Invertible Maps 24 5 Case Study 26 6 Conclusions 27 References 28 ParaGnosis: A Tool for Parallel Knowledge Compilation 31 1 Introduction 31 2 Background 32 2.1 Bayesian Networks 32 2.2 Knowledge Compilation 33 3 Weighted Model Counting Methodologies 36 3.1 Compilation to a Compositional Knowledge Base 37 3.2 Inference 38 4 ParaGnosis 38 4.1 The COMPILER 39 4.2 The INFERENCE ENGINE 40 5 Performance of ParaGnosis 41 6 Discussion 43 References 45 Concurrency 47 Model Checking Futexes 48 1 Introduction 48 2 The Futex System Call 49 3 Modelling the Futex System Call Variants 50 4 Modelling Atomic Operations and Overflow 52 5 Model Checking Futex-based Mutexes 53 5.1 Model Checking Harness and Properties 53 5.2 Incorrect Futex-based Mutex 54 5.3 Correct Futex-based Mutex 56 6 Model Checking Futex-based Condition Variables 60 6.1 Model Checking Harness and Properties 60 6.2 Take 1: Naive and Incorrect 62 6.3 Take 2: Bionic, Unlikely yet Possible Deadlock 62 7 Related Work 63 8 Future Directions 64 References 64 Sound Concurrent Traces for Online Monitoring 66 1 Introduction 66 2 Issues with Linear Traces 69 3 Characterizing a Concurrent Execution 70 4 Sound and Faithful Concurrent Traces 71 5 Obtaining Sound Concurrent Traces 73 5.1 The Reordering Algorithm 73 5.2 Correctness Discussion 74 6 Criteria for Monitorability 75 6.1 Monitor Causal Dependence 76 6.2 Trace Monitorability of Concurrent Executions 77 7 Experimentation and Evaluation 78 8 Related Work 80 9 Conclusion and Future Work 82 References 82 Testing 88 Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks 89 1 Introduction 89 2 Preliminaries 90 3 Related Work 92 4 Motivating Example 93 5 Method Overview 93 6 Layered and Service-Oriented CRN Model Generation 94 7 Shortest Trace Generation 96 8 Generation of Diverse Traces 100 9 Tool Implementation 101 10 Results and Discussion 102 11 Conclusion 105 References 105 Accelerating Black Box Testing with Light-Weight Learning*-12pt 109 1 Introduction 109 2 Preliminaries 111 2.1 The Model 111 2.2 The RPNI Algorithm 111 3 The Algorithm 112 3.1 The Setting 112 3.2 A Modified RPNI Variant: Kernel Construction 113 3.3 The Basic Algorithm 114 3.4 Testing the Black Box Against a Specification 116 4 Experiments 120 4.1 Examples - Basic Algorithm 121 4.2 Examples - Testing the Black Box Against a Specification 123 5 Conclusions 124 References 125 Synthesis 127 WikiCoder: Learning to Write Knowledge-Powered Code 128 1 Introduction 128 2 Knowledge-Powered Programming by Example 130 2.1 Objectives 130 2.2 Milestones 130 2.3 Motivating Examples 132 3 WikiCoder 133 3.1 Compilation 133 3.2 Examples Processing 134 3.3 Search 137 4 Evaluation 137 4.1 Environment 138 4.2 Results on the New Dataset 139 4.3 Comparison with Codex and GPT-3 140 4.4 Results on FlashFill 141 4.5 Limitations 141 4.6 Examples of Programs 142 5 Discussion 142 5.1 Related Work 142 5.2 Contributions and Outlook 143 References 144 Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties 146 1 Introduction 146 2 Illustrative Example 150 3 Background 152 3.1 Reachability Analysis of Hybrid Systems 152 3.2 Temporal Specification 154 4 Verification of Adaptive Simplex Architectures 155 4.1 Setting 155 4.2 Static Verification of the Baseline Controller 156 4.3 Simplex Execution with Proofs on Demand 158 5 Case Study: Autonomous Racing Car 160 6 Conclusion 162 References 163 Explicit-State Model Checking 166 Elimination of Detached Regions in Dependency Graph Verification 167 1 Introduction 167 2 Dependency Graphs 170 3 Local Algorithm with Detached Regions Detection 171 4 Correctness of the Algorithm 175 5 Implementation and Experiments 178 5.1 CTL Benchmark 178 5.2 Games Synthesis Benchmark 180 6 Conclusion 181 References 182 Potency-Based Heuristic Search with Randomness for Explicit Model Checkingpg*-12pt 184 1 Introduction 184 2 Explicit State-Space Search 185 3 Random Potency-First Search (RPFS) 188 4 Experimental Evaluation of RPFS 189 5 Conclusion 190 References 191 GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data 192 1 Introduction 192 2 Workflow and Modelling Language 193 3 Work Distribution and Retrieval Optimisations 196 4 Tool Evaluation 197 References 199 Author Index 202