Model Checking Software: 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings (Lecture Notes in Computer Science, 13255)

✍ Scribed by Owolabi Legunsen (editor), Grigore Rosu (editor)

• Publisher: Springer
• Year: 2022
• Tongue: English
• Leaves: 162
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 28th International Symposium on Model Checking Software, SPIN 2022, held virtually in May 2022.

The 8 full papers were carefully reviewed and selected from 11 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
Automated Consistency Analysis for Legal Contracts
1 Introduction
2 Preliminaries
3 Contract Modeling
3.1 Modeling of an SPA
4 Formalization
4.1 Logical Formalization of Contract Entities
4.2 Formalization of the Bakery SPA
5 Contract Analyses
5.1 Static Analyses
5.2 Dynamic Analyses
6 The ContractCheck Tool
7 Conclusion
References
Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-Attacks
1 Introduction
2 Overview of Our Approach
3 Background: Timed Rebeca and Lingua Franca
4 Abstraction Tool and Monitor Algorithm
4.1 Abstraction Tool
4.2 Monitor Algorithm
5 Case Study: A Temperature Control System
5.1 Tiny Twin
5.2 Attack Types and Detection Capability
6 Related Work
7 Conclusion and Future Work
References
Synthesis of Rigorous Floating-Point Predicates
1 Introduction
2 Motivating Example
3 FPSyn Algorithm
3.1 Step 1: Simplify the Input Expression
3.2 Step 2: Build the Sign Dictionary
3.3 Step 3: Generate the Substitutions List
3.4 Step 4: Derive and Optimize Error-Bound Subexpressions
3.5 Step 5: Apply Double-Layered Substitution
3.6 Step 6: Group Subexpressions Using Tabu Search
3.7 Step 7: Convert Reals into Floating-Points
3.8 Step 8: Remove Single-Use Intermediate Variables
4 Experiments
5 Related Work
References
Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals
1 Introduction
2 Stochastic Timed Transition Systems
3 Temporal Logics
3.1 Signal Temporal Logic
3.2 HPSTL
4 Statistical Model Checking of Hyperproperties
5 Experiments
5.1 Dining Cryptographers
5.2 RSA
6 Conclusion
References
SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks
1 Introduction
2 Background
2.1 Running Example
3 SpecRepair Overview
4 Finding Violations of Safety Specifications
4.1 An Optimization View on Safety Specifications
4.2 Using Optimization to Find Counter-examples
5 Repair Framework
6 Evaluation
6.1 Experimental Setup
6.2 Counter-Example-Based Repair
7 Discussion
8 Conclusion
References
Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench
1 Introduction
2 Background
2.1 Cryptol and SAW
2.2 SHA-3 Overview
3 Proof Outline and Results
3.1 Visual Inspection and Test Vectors
3.2 Memory Layout and Optimized Computation
3.3 Overrides and Keccak
3.4 Results and Summary
4 FIPS 202 Specification in Cryptol
4.1 The for-method
4.2 The while-method
5 OpenSSL Differences
5.1 State Array Structure and Computation
5.2 Constant Lookup Tables
6 Related Work
7 Conclusion
References
Bounded-Memory Runtime Enforcement
1 Introduction
2 Preliminaries and Notations
3 Runtime Enforcement with Unbounded Buffer
4 Bounded-Memory Runtime Enforcement
4.1 Preliminaries for Bounded-Memory Enforcement
4.2 Bounded-Memory Runtime Enforcement: Problem Definition
4.3 Functional Definition
4.4 Enforcement Algorithm
5 Implementation and Evaluation
5.1 Performance Analysis
6 Potential Application Scenarios
7 Related Work
8 Conclusion and Future Work
References
Solving String Theories Involving Regular Membership Predicates Using SAT
1 Introduction
1.1 Related Work
2 Preliminaries
3 Encoding Regular Constraints
3.1 Word-Based Encoding
3.2 Automaton-Based Encoding
4 Empirical Evalutation
4.1 Performance Analysis
4.2 Comparative Benchmark
4.3 Threats to Validity
5 Conclusion
References
Correction to: Bounded-Memory Runtime Enforcement
Correction to: Chapter “Bounded-Memory Runtime Enforcement” in: O. Legunsen and G. Rosu (Eds.): Model Checking Software, LNCS 13255, https://doi.org/10.1007/978-3-031-15077-7_7
Author Index