Model checking software 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings /
This book constitutes the refereed proceedings of the 26th International Symposium on Model Checking Software, SPIN 2019, held in Beijing, China, in July 2019. The 11 full papers presented and 2 demo-tool papers, were carefully reviewed and selected from 29 submissions. Topics covered include formal...
| Corporate Authors: | International SPIN Workshop Beijing, China) |
|---|---|
| Other Authors: | International SPIN Workshop, Biondi, Fabrizio,, Given-Wilson, Thomas (Computer scientist),, Legay, Axel,, SpringerLink (Online service) |
| Format: | eBook |
| Language: | English |
| Published: |
Cham, Switzerland :
Springer,
2019.
|
| Physical Description: |
1 online resource (x, 261 pages) : illustrations (some color). |
| Series: |
Lecture notes in computer science ;
11636. LNCS sublibrary. Theoretical computer science and general issues. |
| Subjects: |
Table of Contents:
- Intro; Preface; Organization; Contents; Model Verification Through Dependency Graphs; 1 Model Verification; 1.1 On-the-Fly Verification; 1.2 Dependency Graphs Related Work; 2 Dependency Graphs; 3 Encoding of Problems into Dependency Graphs; 3.1 Encoding of Strong Bisimulation; 3.2 Encoding of CTL Model Checking; 4 Local Algorithm for Dependency Graphs; 4.1 Optimizations of the Local Algorithm; 4.2 Distributed Implementation of the Local Algorithm; 5 Abstract Dependency Graphs; 6 Applications of Dependency Graphs; References.
- Model Checking Branching Time Properties for Incomplete Markov Chains1 Introduction; 2 qDTMC and qPCTL; 2.1 Discrete Time Markov Chain with Question Marks (qDTMC); 2.2 qPCTL; 3 qPCTL Model Checking; 4 Implementation and Results; 5 Conclusion and Future Work; References; A Novel Decentralized LTL Monitoring Framework Using Formula Progression Table; 1 Introduction; 2 The Decentralized LTL Monitoring Problem; 3 Simplification Tables for Boolean Formulas; 4 Progression Tables for LTL Formulas; 5 Simplifications; 6 From Simplified Formula to Original Formula.
- 7 Using Progression Tables in Decentralized Monitoring8 Experiments; 8.1 Benchmarks for Patterns of Formulas; 9 Related Work; 10 Conclusion and Future Work; References; From Dynamic State Machines to Promela; 1 Introduction; 2 Dynamic State Machines; 2.1 DSTM Semantics; 3 From DSTM to Promela; 3.1 Encoding the DSTM Vertical Hierarchy; 3.2 From Flat DSTM to Promela; 3.3 Promela Encoding; 4 Conclusions; References; String Abstraction for Model Checking of C Programs; 1 Introduction; 1.1 Related Work; 1.2 Paper Contribution; 2 M-String; 2.1 Concrete Domain; 2.2 Abstract Domain.
- 2.3 Abstract Semantics3 Program Abstraction; 3.1 Compilation-Based Approach; 3.2 Syntactic Abstraction; 3.3 Aggregate Domains; 3.4 Semantic Abstraction; 3.5 Abstract Operations; 4 Instantiating M-String; 4.1 Symbolic Scalar Values; 4.2 Concrete Characters, Symbolic Bounds; 4.3 Implementation; 5 Experimental Evaluation; 6 Conclusion; References; Swarm Model Checking on the GPU; 1 Introduction; 2 Background; 2.1 GPU Hardware Model; 2.2 CUDA Programming Model; 2.3 SPIN Model Checker; 2.4 Swarm Verification; 3 Swarm Verification via the Grapple Model Checker; 4 Experimental Results.
- 4.1 WP Benchmark4.2 Dining Philosophers Model; 4.3 Large-Scale Results; 5 Related Work; 6 Conclusions; References; Statistical Model Checking of Complex Robotic Systems; 1 Introduction; 2 Preliminaries; 2.1 G0Tto0enoM3; 2.2 UPPAAL; 2.3 UPPAAL-SMC; 3 Formalizing G0Tto0enoM3; 3.1 Timed Transition Systems; 3.2 Syntax and Syntactical Restrictions of a G0Tto0enoM3 Component; 3.3 Operational Semantics of a G0Tto0enoM3 Component; 4 Translation; 5 Automatic Mapping; 5.1 Mapping to UPPAAL; 5.2 Automatic Synthesis; 6 Verification Results; 6.1 Model Checking; 6.2 Statistical Model Checking.