19th International SPIN Workshop
on Model Checking of Software
on Model Checking of Software
Oxford, 23-24 July 2012
The programme for SPIN 2012 is as follows.
| 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 |
| 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 |