Model checking software : 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings /: 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings. (2019)

• Record Type: Book
• Other Titles: SPIN 2019
• Further Information: Note: Fabrizio Biondi, Thomas Given-Wilson, Axel Legay (eds.).
• Editors: Biondi, Fabrizio; Given-Wilson, Thomas; Legay, Axel
• Other Names: International SPIN Workshop, 26th
• 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
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2019
• Extent: 1 online resource (x, 261 pages), illustrations (some color)
• Subjects: 005.1/4; Computer software -- Verification -- Congresses; Software engineering -- Congresses; Computer software -- Testing -- Congresses; Electronic books; Electronic books
• Languages: English
• ISBNs: 9783030309237; 3030309231
• Related ISBNs: 9783030309220
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed October 9, 2019).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.