Model Checking Software

1. Front Matter

   PDF

2. Invited Contributions

   1. Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials

      • Thomas Ball, Nikolaj Bjørner, Leonardo de Moura, Kenneth L. McMillan, Margus Veanes

      Pages 1-6

   2. High-Coverage Symbolic Patch Testing

      • Paul Dan Marinescu, Cristian Cadar

      Pages 7-21

   3. Towards Automatic Synthesis of Software Verification Tools

      • Andrey Rybalchenko

      Pages 22-22

   4. Mining Models

      • Andreas Zeller

      Pages 23-23

3. Model Checking Techniques

   1. Counterexample Explanation by Anomaly Detection

      • Stefan Leue, Mitra Tabaei Befrouei

      Pages 24-42

   2. Combining the Sweep-Line Method with the Use of an External-Memory Priority Queue

      • Sami Evangelista, Lars Michael Kristensen

      Pages 43-61

   3. A Compositional Minimization Approach for Large Asynchronous Design Verification

      • Hao Zheng, Emmanuel Rodriguez, Yingying Zhang, Chris Myers

      Pages 62-79

4. Parallel Model Checking 1

   1. On Parallel Software Verification Using Boolean Equation Systems

      • Alexander Ditter, Milan Češka, Gerald Lüttgen

      Pages 80-97

   2. Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking

      • Anton J. Wijs, Dragan Bošnački

      Pages 98-116

5. Case Studies

   1. Gossiping Girls Are All Alike

      • Theo C. Ruys, Pim Kars

      Pages 117-136

   2. Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid

      • Shravan Garlapati, Sandeep K. Shukla

      Pages 137-154

6. Parallel Model Checking 2

   1. Parallelizing the Spin Model Checker

      • Gerard J. Holzmann

      Pages 155-171

   2. Parallel Model Checking Using Abstraction

      • Ethan Burns, Rong Zhou

      Pages 172-190

7. Model Checking for Concurrency

   1. McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking

      • Reng Zeng, Zhuo Sun, Su Liu, Xudong He

      Pages 191-207

   2. Parameterized Model Checking of Fine Grained Concurrency

      • Divjyot Sethi, Muralidhar Talupur, Daniel Schwartz-Narbonne, Sharad Malik

      Pages 208-226

8. Tool Demonstrations

   1. mctau: Bridging the Gap between Modest and UPPAAL

      • Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, Holger Hermanns

      Pages 227-233

   2. FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation

      • Heinz Riener, Görschwin Fey

      Pages 234-240

   3. Model Checking DSL-Generated C Source Code

      • Martin Sulzmann, Axel Zechner

      Pages 241-247

   4. SMTInterpol: An Interpolating SMT Solver

      • Jürgen Christ, Jochen Hoenicke, Alexander Nutz

      Pages 248-254

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.

• automated debugging
• formal testing
• model-driven engineering
• probabilistic model checking
• software verification

• Department of Computing, Imperial College London, London, UK

  Alastair Donaldson

• School of Computer Science, University of Birmingham, Edgbaston, UK

  David Parker

Policies and ethics