Model Checking Software: 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings

✍ Scribed by Thomas Ball, Nikolaj Bjørner, Leonardo de Moura, Kenneth L. McMillan, Margus Veanes (auth.), Alastair Donaldson, David Parker (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2012
• Tongue: English
• Leaves: 271
• Series: Lecture Notes in Computer Science 7385
• Edition: 1
• Category: Library

✦ Synopsis

This book constitutes the thoroughly refereed proceedings of the 19th International SPIN workshop on Model Checking Software, SPIN 2012, held in Oxford, UK, in July 2012. The 11 revised full papers presented together with 5 tool papers and 4 invited talks were carefully reviewed and selected from 30 submissions. The papers are grouped in topical sections on model checking techniques; parallel model checking; case studies; model checking for concurrency; and tool demonstrations.

✦ Table of Contents

Front Matter....Pages -
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials....Pages 1-6
High-Coverage Symbolic Patch Testing....Pages 7-21
Towards Automatic Synthesis of Software Verification Tools....Pages 22-22
Mining Models....Pages 23-23
Counterexample Explanation by Anomaly Detection....Pages 24-42
Combining the Sweep-Line Method with the Use of an External-Memory Priority Queue....Pages 43-61
A Compositional Minimization Approach for Large Asynchronous Design Verification....Pages 62-79
On Parallel Software Verification Using Boolean Equation Systems....Pages 80-97
Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking....Pages 98-116
Gossiping Girls Are All Alike....Pages 117-136
Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid....Pages 137-154
Parallelizing the Spin Model Checker....Pages 155-171
Parallel Model Checking Using Abstraction....Pages 172-190
McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking....Pages 191-207
Parameterized Model Checking of Fine Grained Concurrency....Pages 208-226
mctau: Bridging the Gap between Modest and UPPAAL....Pages 227-233
FAuST : A Framework for Formal Verification, Automated Debugging, and Software Test Generation....Pages 234-240
Model Checking DSL-Generated C Source Code....Pages 241-247
SMTInterpol: An Interpolating SMT Solver....Pages 248-254
S2N: Model Transformation from SPIN to NuSMV....Pages 255-260
Back Matter....Pages -

✦ Subjects

Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs