| Description |
1 online resource (x, 261 pages) : illustrations (some color) |
| Series |
Lecture notes in computer science ; 11636 |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 11636.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| 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 |
| Summary |
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 verification techniques for automated analysis of software; formal analysis for modeling languages, such as UML/state charts; formal specification languages, temporal logic, design-by-contract; model checking, automated theorem proving, including SAT and SMT; verifying compilers; abstraction and symbolic execution techniques; and much more. -- Provided by publisher |
| Notes |
International conference proceedings |
|
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed October 9, 2019) |
| SUBJECT |
SPIN (Computer file) -- Congresses
|
|
SPIN (Computer file) fast |
| Subject |
Computer software -- Verification -- Congresses
|
|
Software engineering -- Congresses
|
|
Computer software -- Testing -- Congresses
|
|
Computer software -- Testing
|
|
Computer software -- Verification
|
|
Software engineering
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Biondi, Fabrizio, editor
|
|
Given-Wilson, Thomas, editor
|
|
Legay, Axel, editor.
|
| ISBN |
9783030309237 |
|
3030309231 |
|
