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

Description

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 Organization Contents Binary Decision Diagrams Efficient Implementation of LIMDDs for Quantum Circuit Simulation 1 Introduction 2 Background 2.1 Quantum States and Operations 2.2 Classical Quantum Circuit Simulation 2.3 Verification of Quantum Circuits 3 Motivation 3.1 Quantum Multiple-valued Decision Diagrams (QMDDs) 3.2 Local Invertible Map Decision Diagrams (LIMDDs) 3.3 The Need for a LIMDD Implementation 4 Implementation of LIMDDs 4.1 Established Techniques 4.2 Implementing Local Invertible Maps 5 Case Study 6 Conclusions References ParaGnosis: A Tool for Parallel Knowledge Compilation 1 Introduction 2 Background 2.1 Bayesian Networks 2.2 Knowledge Compilation 3 Weighted Model Counting Methodologies 3.1 Compilation to a Compositional Knowledge Base 3.2 Inference 4 ParaGnosis 4.1 The COMPILER 4.2 The INFERENCE ENGINE 5 Performance of ParaGnosis 6 Discussion References Concurrency Model Checking Futexes 1 Introduction 2 The Futex System Call 3 Modelling the Futex System Call Variants 4 Modelling Atomic Operations and Overflow 5 Model Checking Futex-based Mutexes 5.1 Model Checking Harness and Properties 5.2 Incorrect Futex-based Mutex 5.3 Correct Futex-based Mutex 6 Model Checking Futex-based Condition Variables 6.1 Model Checking Harness and Properties 6.2 Take 1: Naive and Incorrect 6.3 Take 2: Bionic, Unlikely yet Possible Deadlock 7 Related Work 8 Future Directions References Sound Concurrent Traces for Online Monitoring 1 Introduction 2 Issues with Linear Traces 3 Characterizing a Concurrent Execution 4 Sound and Faithful Concurrent Traces 5 Obtaining Sound Concurrent Traces 5.1 The Reordering Algorithm 5.2 Correctness Discussion 6 Criteria for Monitorability 6.1 Monitor Causal Dependence 6.2 Trace Monitorability of Concurrent Executions 7 Experimentation and Evaluation 8 Related Work 9 Conclusion and Future Work References Testing Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks 1 Introduction 2 Preliminaries 3 Related Work 4 Motivating Example 5 Method Overview 6 Layered and Service-Oriented CRN Model Generation 7 Shortest Trace Generation 8 Generation of Diverse Traces 9 Tool Implementation 10 Results and Discussion 11 Conclusion References Accelerating Black Box Testing with Light-Weight Learning*-12pt 1 Introduction 2 Preliminaries 2.1 The Model 2.2 The RPNI Algorithm 3 The Algorithm 3.1 The Setting 3.2 A Modified RPNI Variant: Kernel Construction 3.3 The Basic Algorithm 3.4 Testing the Black Box Against a Specification 4 Experiments 4.1 Examples - Basic Algorithm 4.2 Examples - Testing the Black Box Against a Specification 5 Conclusions References Synthesis WikiCoder: Learning to Write Knowledge-Powered Code 1 Introduction 2 Knowledge-Powered Programming by Example 2.1 Objectives 2.2 Milestones 2.3 Motivating Examples 3 WikiCoder 3.1 Compilation 3.2 Examples Processing 3.3 Search 4 Evaluation 4.1 Environment 4.2 Results on the New Dataset 4.3 Comparison with Codex and GPT-3 4.4 Results on FlashFill 4.5 Limitations 4.6 Examples of Programs 5 Discussion 5.1 Related Work 5.2 Contributions and Outlook References Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties 1 Introduction 2 Illustrative Example 3 Background 3.1 Reachability Analysis of Hybrid Systems 3.2 Temporal Specification 4 Verification of Adaptive Simplex Architectures 4.1 Setting 4.2 Static Verification of the Baseline Controller 4.3 Simplex Execution with Proofs on Demand 5 Case Study: Autonomous Racing Car 6 Conclusion References Explicit-State Model Checking Elimination of Detached Regions in Dependency Graph Verification 1 Introduction 2 Dependency Graphs 3 Local Algorithm with Detached Regions Detection 4 Correctness of the Algorithm 5 Implementation and Experiments 5.1 CTL Benchmark 5.2 Games Synthesis Benchmark 6 Conclusion References Potency-Based Heuristic Search with Randomness for Explicit Model Checkingpg*-12pt 1 Introduction 2 Explicit State-Space Search 3 Random Potency-First Search (RPFS) 4 Experimental Evaluation of RPFS 5 Conclusion References GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data 1 Introduction 2 Workflow and Modelling Language 3 Work Distribution and Retrieval Optimisations 4 Tool Evaluation References Author Index