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:


The programme for SPIN 2012 is as follows.

Day 1: Monday 23 July 2012
8.30 Registration & Coffee
9.00 9.15 Welcome
Invited talk: Tom Ball
Beyond First-order Satisfaction: Fixed points, Interpolants, Automata and Polynomials
10.15 Coffee
10.45 Model Checking Techniques
Stefan Leue and Mitra Tabaei Befrouei
Counterexample Explanation by Anomaly Detection
Sami Evangelista and Lars Kristensen
Combining the Sweep-Line Method with the use of an External-memory Priority Queue
Hao Zheng, Emmanuel Rodriguez, Yingying Zhang and Chris Myers
A Compositional Minimization Approach for Large Asynchronous Design Verification
12.15 Lunch
13.30 Invited tutorial: Cristian Cadar
How to Crash Your Code using Dynamic Symbolic Execution
14.30 Coffee
15.00 Parallel Model Checking 1
Alexander Ditter, Milan Ceska and Gerald Lüttgen
On Parallel Software Verification using Boolean Equation Systems
Anton J. Wijs and Dragan Bosnacki
Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking
16.00 Tool Presentations
Juergen Christ, Jochen Hoenicke and Alexander Nutz
SMTInterpol – An Interpolating SMT Solver
Jonathan Bogdoll, Alexandre David, Arnd Hartmanns and Holger Hermanns
mctau: Bridging the Gap between Modest and UPPAAL
16.40 Close
Workshop banquet

Day 2: Tuesday 24 July 2012
8.30 Coffee
9.00 Invited talk: Andreas Zeller
Mining Models
10.00 Case Studies
Theo Ruys and Pim Kars
Gossiping Girls Are All Alike
Shravan Garlapati and Sandeep Shukla
Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid
11.00 Coffee
11:30 Parallel Model Checking 2
Gerard Holzmann
Parallelizing the Spin Model Checker
Ethan Burns and Rong Zhou
Parallel Model Checking using Abstraction
12.30 Tool Presentation
Yong Jiang and Zongyan Qiu
S2N: Model Transformation from SPIN to NuSMV
12.50 Lunch
14:00 Invited Talk: Andrey Rybalchenko
Towards Automatic Synthesis of Software Verification Tools
15:00 Coffee
15:30 Model Checking for Concurrency
Reng Zeng, Zhuo Sun, Su Liu and Xudong He
McPatom: A Predictive Analysis Tool for Atomicity Violation using Model Checking
Divjyot Sethi, Murali Talupur, Sharad Malik and Daniel Schwartz-Narbonne
Parameterized Model Checking of Fine Grained Concurrency
16.30 Tool Presentations
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
17:10 Close