Model checking software : 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings / Fabrizio Biondi, Thomas Given-Wilson, Axel Legay (eds.).
Contributor(s): Biondi, Fabrizio [editor.] | Given-Wilson, Thomas [editor.] | Legay, Axel [editor.]Material type: TextSeries: SerienbezeichnungLecture notes in computer science: 11636.; LNCS sublibrary: Publisher: Cham, Switzerland : Springer, 2019Description: 1 online resource (x, 261 pages) : illustrations (some color)Content type: text Media type: computer Carrier type: online resourceISBN: 9783030309237; 3030309231Other title: SPIN 2019Subject(s): SPIN (Computer file) -- Congresses | SPIN (Computer file) | Computer software -- Verification -- Congresses | Software engineering -- Congresses | Computer software -- Testing -- Congresses | Computer software -- Testing | Computer software -- Verification | Software engineeringGenre/Form: Electronic books. | Conference papers and proceedings. DDC classification: 005.1/4 LOC classification: QA76.76.V47Online resources: Click here to access online
|Item type||Current location||Collection||Call number||Status||Date due||Barcode||Item holds|
International conference proceedings.
Includes author index.
Online resource; title from PDF title page (SpringerLink, viewed October 9, 2019).
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
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.