Model Checking Software

Name: Model Checking Software | 19th International SPIN Workshop, Oxford, UK, July 23-24, 2012. Proceedings
Brand: Springer
Price: 48.14 EUR
Availability: OnlineOnly

19th International SPIN Workshop, Oxford, UK, July 23-24, 2012. Proceedings

Alastair Donaldson David Parker(Herausgeber*in)

Springer (Verlag)

1. Auflage

Erschienen am 18. Juli 2012

X, 261 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31759-0 (ISBN)

48,14 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Preface
Organization
Table of Contents
Invited Contributions
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials
Introduction
Fixed Points and Z
Interpolants
Symbolic Automata
Polynomials
References
High-Coverage Symbolic Patch Testing
Introduction
Overview
Design
Implementation
Experimental Evaluation
Related Work
Discussion and Future Work
References
Towards Automatic Synthesis of Software Verification Tools
References
Mining Models
Reference
Model Checking Techniques
Counterexample Explanation by Anomaly Detection
Introduction
A Motivating Example
Mining Sequential Patterns for Counterexample Explanation
Sequential Pattern Mining
Challenges in Applying Sequential Pattern Mining Algorithms
Counterexample Explanation Method
Generation of the Good and the Bad Datasets
Contrasting Sequence Sets
Experimental Results
Comparison with the Work by Groce and Visser
Conclusion
References
Combining the Sweep-Line Method with the Use of an External-Memory Priority Queue
Introduction
The Sweep-Line Method and Motivation
Using an External Memory Priority Queue
Description of the Algorithm
External Priority Queue Data Structure
I/O complexity
Experimental Evaluation
Conclusions and Future Work
References
A Compositional Minimization Approach for Large Asynchronous Design Verification
Introduction
Preliminaries
State Graphs
Correctness Definition
State Graph Reductions
Observably Equivalent Reduction
Redundancy Removal
Comparison between Reduction and Abstraction
Experimental Results
Conclusion
References
Parallel Model Checking 1
On Parallel Software Verification Using Boolean Equation Systems
Introduction
Fixed Points and Boolean Equation Systems
Basic Fixed Point Algorithm and Parallelization
Experimental Evaluation
Conclusions and Future Work
References
Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking
Introduction
GPU Preliminaries
Structures of Transition Probability Matrices and BFS Reindexing
Breadth-First Search Reindexing of the States
Coalescing Matrix Data Access
Sparse Matrix Representation
A Full-Warp SpMV Algorithm
A Half-Warp SpMV Algorithm
Experimental Results
Conclusions, Prospects and Related Work
References
Case Studies
Gossiping Girls Are All Alike
Introduction
Initial Attempts
Channel of Knowledge
TopSPIN
Bliss
Experiments
Conclusions
References
Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid
Introduction
Distance Relaying Protection Scheme
Previous Work
Modelling Behaviour
Verification
Observations
Conclusion
References
Parallel Model Checking 2
Parallelizing the Spin Model Checker
Introduction
Breadth-First Search
Parallel Breadth-First Search
Lock Avoidance
Synchronization and Termination
Partial Order Reduction
An Extension for Liveness
Measurements
Beem Models
Additional Spin Models
Background Load.
Larger Models
Liveness
Conclusion
References
Parallel Model Checking Using Abstraction
Introduction
Depth-First versus Breadth-First Search
Hash-Distributed Breadth-First Search
Disadvantages
Abstraction-Based Hashing
Parallel Structured Duplicate Detection
Abstraction for Model Checking
Experimental Results
Multi-core Depth-First Search
Effect of Delaying Duplicate Detection
Effect of Conservative Partial-Order Reduction
Overall Performance
External-Memory PSDD
Discussion and Related Work
Conclusion and Future Work
References
Model Checking for Concurrency
McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking
Introduction
Extracting Partial Order Thread Models from Multi-thread Program Executions
Description of the Partial Order Thread Model
Implementation of the Partial Order Thread Model
Defining and Encoding Unserializable Interleaving Patterns between Two Threads
Three-Access and Four-Access Atomicity Violation
Patterns of Two-Thread Atomicity Violations involving any Number of Accesses
Automatically Encoding Atomicity Violation Patterns into Linear Time Temporal Logic (LTL) Formulas
Predictive Analysis of Atomicity Violation Using Model Checking
Soundness and Completeness of McPatom
Using Spin Model Checker to Find Atomicity Violation Traces
Mapping the Violations Reported in Spin to the Original Program
Evaluation
Related Works
Conclusion
References
Parameterized Model Checking of Fine Grained Concurrency
Introduction
The CMP Method
Framework Description
Main Contributions
Related Work
Encoding Concurrent Data Structures as Parameterized Systems
Running Example: Lazy List Based Concurrent Set
Encoding the Lazy Set in Murphi
Parameterized Model Checking Using the CMP Method
Verifying the Lazy Set Algorithm
Automatic Generation of Candidate Lemmas
Experiments
Verification Experience: Candidate Lemmas
Conclusion and Future Work
References
Tool Demonstrations
mctau: Bridging the Gap between Modest and UPPAAL
Introduction
Bridging the Gap
The mctau Tool
Evaluation
Conclusion
References
FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation
Introduction
Formalizing LLVM-IR into Logic Using BMC
Applications
Formal Verification
Automatic Debugging
Test Generation
Related Work
Conclusions
References
Model Checking DSL-Generated C Source Code
Introduction
DSL Tool-Chain Overview
SPIN-DSL Integration
Industrial Case Study: Motor-Start Stop (MSA)
References
SMTInterpol: An Interpolating SMT Solver
Introduction
Architecture of SMTInterpol
How to Use SMTInterpol
Interpolation for SMTLIB Logics
Experiments
Future Work
Conclusion
References
S2N: Model Transformation from SPIN to NuSMV
Introduction
Translation Techniques
Marking
Variable Declaration
Initialization and Transition
Constraint Expression
Tool and Experiments
Features Supported
Experiments
Conclusion and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken