[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Call for Participation: SPIN 2012 - 19th International SPIN Workshop on Model Checking Software

Apologies for multiple copies.

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


Registration is now open!

For the full programme, and to register, visit:



Invited speakers

* Tom Ball, Microsoft Research, Redmond. Beyond First-order
Satisfaction: Fixed points, Interpolants, Automata and Polynomials.

* Andrey Rybalchenko, TU Munich. Towards Automatic Synthesis of
Software Verification Tools

* Andreas Zeller, Saarland University. Mining Models

Invited tutorial

* Cristian Cadar, Imperial College London. How to Crash Your Code
using Dynamic Symbolic Execution

Regular papers

* Gerard Holzmann. Parallelizing the Spin Model Checker

* Ethan Burns and Rong Zhou. Parallel Model Checking using

* 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

* 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

* 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

* 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

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


* ARM (http://www.arm.com)
* Codeplay Software (http://www.codeplay.com)
* Microsoft Research (http://research.microsoft.com/en-us)
* Monoidics (http://www.monoidics.com)