International SPIN Symposium
on Model Checking of Software
Stony Brook, NY, USA, 8-9 July 2013
Marking the 20th Anniversary of the International SPIN Workshop


April 2013
A block of rooms has been reserved at the Campus Hotel (Hilton Garden Inn), just a few minutes walk from the Carles B. Wang Asian-American Center. Click here to book for the hotel with the SPIN rate.
March 2013
Spin 2013 will overlap with 24th International Conference on Game Theory at Stony Brook University.

For those of you interested in game theory, you can extend your stay at Stony Brook to hear about the latest developments in this field from leading experts.

October 2012
Best Paper Award offered by NVIDIA.
October 2012
Special Issue on STTT - International Journal on Software Tools for Technology Transfer.
September 2012
IBM, Microsoft and NEC joined as our sponsors.
July 2012
Program Committee announced.
June 2012
Work in Progress for Spin 2013.



The provisional programme for SPIN 2013 is as follows.

Day 1: Monday 8 July 2013
8.30 Registration
9.00 9.15 Welcome, Opening Remarks
Invited talk: Gerard Holzmann
Proving properties of concurrent C programs
10.15 Coffee Break
10.45 Regression Verification using Impact Summaries
John Backes, Suzette Person, Neha Rungta and Oksana Tkachuk
Expression Reduction from Programs in a Symbolic Binary Executor
Anthony Romano and Dawson Engler
Property-Driven Benchmark Generation
Bernhard Steffen, Malte Isberner, Stefan Naujokat, Tiziana Margaria and Maren Geske
COMPLeTe - A COMmunication Protocol vaLidation Toolchain using Formal and Model-Based Specifications and Descriptions (Tool paper)
Sven Groening, Christopher Rosas and Christian Wietfeld
12.30 Lunch
14.00 Probabilistic Verification of Coordinated Multi-Robot Missions
Sagar Chaki and Joseph Giampapa
On the Synergy of Probabilistic Causality Computation and Causality Checking
Florian Leitner-Fischer and Stefan Leue
On-the-Fly Control Software Synthesis
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci
Synthesizing Controllers for Automation Tasks with Performance Guarantees (Tool Paper)
Chih-Hong Cheng, Michael Geisinger and Christian Buckl
15.45 Coffee Break
16.15 Guard-based Partial Order Reduction
Alfons Laarman, Elwin Pater and Jaco van de Pol
Local Model Checking of Weighted CTL with Upper-Bound Constraints
Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba and Lars Kærlund Østergaard
Compositional Approach to Suspension and and Other Improvements to LTL Translation.
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmir Kretinsky and Jan Strejcek
17.45 Close
18:30-22:00 Workshop banquet

Day 2: Tuesday 9 July 2013
9.00 Invited talk: Dirk Beyer
Conditional Model Checking
10.00 Coffee Break
10.30 Automatic Equivalence Checking of UF+IA Programs
Nuno P. Lopes and Jose Monteiro
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder
Spin the Groove: Specification of Link Reversal Routing as Graph Transformations
Giorgio Delzanno and Riccardo Traverso
12.00 Lunch Break (SCGP Cafe)
14.00 Abstraction-Based Guided Search for Hybrid Systems
Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle
Verifying a Quantitative Relaxation of Linearizability via Refinement
Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang
Model Checking Unbounded Concurrent Lists
Divjyot Sethi, Murali Talupur and Sharad Malik
15:30 Coffee Break
16:00 A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci
Mining Sequential Patterns to Explain Concurrent Counterexamples
Stefan Leue and Mitra Tabaei Befrouei
Error-Completion in Interface Theories
Stavros Tripakis, Christos Stergiou, Manfred Broy and Edward Lee
17:30 Close

SPIN 2013 gratefully acknowledges the support from the following sponsors: