19th International SPIN Workshop
on Model Checking of Software
Oxford, 23-24 July 2012


May 2012
The provisional programme is now online.
May 2012
Registration is now open.


SPIN 2012 is sponsored by:

Accepted Papers

The list of accepted papers is as follows:

Regular papers
  • Sami Evangelista and Lars Kristensen.
    Combining the Sweep-Line Method with the use of an External-memory Priority Queue
  • Divjyot Sethi, Murali Talupur, Sharad Malik and Daniel Schwartz-Narbonne.
    Parameterized Model Checking of Fine Grained Concurrency
  • Alexander Ditter, Milan Ceska and Gerald Lüttgen.
    On Parallel Software Verification using Boolean Equation Systems
  • Gerard Holzmann.
    Parallelizing the Spin Model Checker
  • Stefan Leue and Mitra Tabaei Befrouei.
    Counterexample Explanation by Anomaly Detection
  • Shravan Garlapati and Sandeep Shukla.
    Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid
  • Anton J. Wijs and Dragan Bosnacki.
    Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking
  • Ethan Burns and Rong Zhou.
    Parallel Model Checking using Abstraction
  • Reng Zeng, Zhuo Sun, Su Liu and Xudong He.
    McPatom: A Predictive Analysis Tool for Atomicity Violation using Model Checking
  • Hao Zheng, Emmanuel Rodriguez, Yingying Zhang and Chris Myers.
    A compositional Minimization Approach for Large Asynchronous Design Verification
  • Theo Ruys and Pim Kars.
    Gossiping Girls Are All Alike
Tool papers
  • Jonathan Bogdoll, Alexandre David, Arnd Hartmanns and Holger Hermanns.
    mctau: Bridging the Gap between Modest and UPPAAL
  • Heinz Riener and Goerschwin Fey.
    FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation
  • Martin Sulzmann and Axel Zechner.
    Model Checking DSL-Generated C Source Code
  • Juergen Christ, Jochen Hoenicke and Alexander Nutz.
    SMTInterpol – An Interpolating SMT Solver
  • Yong Jiang and Zongyan Qiu.
    S2N: Model Transformation from SPIN to NuSMV