Model Checking Software: 27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings (Theoretical Computer Science and General Issues)

✍ Scribed by Alfons Laarman (editor), Ana Sokolova (editor)

• Publisher: Springer
• Year: 2021
• Tongue: English
• Leaves: 199
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 27th International Symposium on Model Checking Software, SPIN 2021, held virtually in July 2021.

The 3 full papers, 4 tool papers, and 1 case study presented together with 2 invited talks were carefully reviewed and selected from 20 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.

✦ Table of Contents

Preface
Organization
Contents
Invited Talks
The Marriage Between Safety and Cybersecurity: Still Practicing
1 Introduction
2 Background
3 Formalisms for Safety-Security Co-analysis: An Overview
3.1 The Formalisms
3.2 Findings
4 Attack Trees Versus Fault Trees
4.1 Attack Trees Versus Fault Trees
4.2 The Static Case
4.3 Semantics
4.4 Metrics for Attack and Fault Trees
5 Analysis Algorithms for Attack and Fault Trees
5.1 Algorithms for Tree-Shaped DTs
5.2 Algorithms for DAG-Shaped DTs
5.3 Research Gaps
6 Conclusions
References
A Hands-On Introduction to Spatial Model Checking Using VoxLogicA
1 Introduction
2 Using VoxLogicA: Practicalities
2.1 The Declarative Language ImgQL
2.2 Loading and Saving Models
2.3 Anatomy of VoxLogicA Logs
2.4 Working with Datasets
3 Topological Properties and Reachability
4 Global Properties and Region Calculi
5 Advanced Topics: Background Removal, Distance, Filtering, Texture Similarity
6 Related Work
7 Outlook
References
Model Checking
Accelerating the Computation of Dead and Concurrent Places Using Reductions
1 Introduction
2 Petri Nets and Polyhedral Abstraction
3 Token Flow Graphs
4 Dimensionality Reduction Algorithm
5 Experimental Results
6 Conclusion and Further Work
References
Spotlight Abstraction in Model Checking Real-Time Task Schedulability
1 Introduction
2 Related Work
3 Encoding RTOS Scheduler Models as Timed Automata
3.1 A Scheduler Model
3.2 The Abstract Task Models
4 An Example: Model Checking Schedulability for FIFO RTOS Scheduler
5 Model Checking Real-Time Queues Using Spotlight Abstraction
5.1 The Abstraction Algorithm Commences
5.2 Calling the Reachability Analysis Algorithm
5.3 The Abstraction Algorithm Resumes
6 Experimental Results
7 Conclusion and Outlook
References
Verifying Pipeline Implementations in OpenMP
1 Introduction
2 Using OpenMP to Implement Pipelines
3 Verifying Correctness of Pipeline Implementations
3.1 Constructing Task Dependency Graphs
3.2 Inspecting RAW and WAR Dependencies
3.3 Checking WAW Dependencies and I/O Availability
3.4 Handling of Loop Header
3.5 Implementation
4 Evaluation
4.1 Experimental Results
5 Related Work
6 Conclusion
References
Tool Papers
C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs
1 Introduction and Motivation
2 Systems: From Specification to Verification
2.1 Trace Execution Properties
2.2 Probabilistic Verification
2.3 Implementation: Plasma Lab
3 Architecture of C-SMC
3.1 Simulator
3.2 Checker
3.3 C-SMC Configuration
3.4 Running C-SMC
4 Use Cases
5 Examples and Evaluation
5.1 Methodology
5.2 Results
6 Conclusion and Future Work
References
PatEC: Pattern-Based Equivalence Checking
1 Introduction
2 Background
3 Determining Equivalence for DoAll and Reduction
4 Evaluation
4.1 Experimental Setup
4.2 Experiments
5 Related Work
6 Conclusion
References
Go2Pins: A Framework for the LTL Verification of Go Programs
1 Introduction and Motivation
2 Go2Pins: Overview
3 Implementation Details
3.1 Core Translation: Func. Def. to Transform
3.2 Handling Concurrency: Goroutines and Unbuffered Channels
4 Abstraction with Black-Box Transitions
4.1 Overview of Black-Box Transitions
4.2 User-Defined Black-Box Transitions
5 Using Go2Pins on Go Programs
6 Benchmark
7 Related Work
8 Conclusion
References
Probabilistic Model Checking of Randomized Java Code
1 Introduction
2 JPF-Label
3 JPF-Probabilistic
4 Our Converter
5 Monte Carlo Algorithms
6 Very Large and Infinite State Spaces
7 Other Quantitative Properties
8 Overhead
9 Conclusion
References
Case Studies
A Model-Checked I2C Specification
1 Introduction
2 Background
3 Related Work
4 Approach and Tools
4.1 Programming Model, DSL, and Backends
4.2 Calculus
5 The I2C Model
5.1 Layering of I2C
5.2 Layer 0: Electrical Layer
5.3 Layer 1: Symbol Layer
5.4 L2: Byte Layer
5.5 L3: Transaction Layer
5.6 L4: Driver
5.7 L5: World
6 Evaluation
6.1 Verification Runtime
6.2 Execution on a Raspberry Pi
7 Conclusion and Future Work
References
Author Index