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 Charles 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.


Accepted Papers

The list of accepted papers is as follows:

Regular papers:
  • Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci.
    A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software
  • Nuno P. Lopes and Jose Monteiro.
    Automatic Equivalence Checking of UF+IA Programs.
  • Alfons Laarman, Elwin Pater and Jaco van de Pol.
    Guard-based Partial Order Reduction.
  • Divjyot Sethi, Murali Talupur and Sharad Malik.
    Model Checking Unbounded Concurrent Lists.
  • Sagar Chaki and Joseph Giampapa.
    Probabilistic Verification of Coordinated Multi-Robot Missions.
  • Anthony Romano and Dawson Engler.
    Expression Reduction from Programs in a Symbolic Binary Executor.
  • John Backes, Suzette Person, Neha Rungta and Oksana Tkachuk.
    Regression Verification using Impact Summaries.
  • Stefan Leue and Mitra Tabaei Befrouei.
    Mining Sequential Patterns to Explain Concurrent Counterexamples.
  • Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci.
    On-the-Fly Control Software Synthesis.
  • Florian Leitner-Fischer and Stefan Leue.
    On the Synergy of Probabilistic Causality Computation and Causality Checking.
  • Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmir Kretinsky and Jan Strejcek.
    Compositional Approach to Suspension and and Other Improvements to LTL Translation.
  • Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder.
    Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms.
  • Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle.
    Abstraction-Based Guided Search for Hybrid Systems.
  • Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang.
    Verifying a Quantitative Relaxation of Linearizability via Refinement.
  • Giorgio Delzanno and Riccardo Traverso.
    Spin the Groove: Specification of Link Reversal Routing as Graph Transformations.
  • Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba and Lars Kærlund Østergaard.
    Local Model Checking of Weighted CTL with Upper-Bound Constraints.
  • Stavros Tripakis, Christos Stergiou, Manfred Broy and Edward Lee.
    Error-Completion in Interface Theories.
  • Bernhard Steffen, Malte Isberner, Stefan Naujokat, Tiziana Margaria and Maren Geske.
    Property-Driven Benchmark Generation.
Tool paper:
  • Sven Groening, Christopher Rosas and Christian Wietfeld.
    COMPLeTe - A COMmunication Protocol vaLidation Toolchain using Formal and Model-Based Specifications and Descriptions.
  • Chih-Hong Cheng, Michael Geisinger and Christian Buckl.
    Synthesizing Controllers for Automation Tasks with Performance Guarantees.

SPIN 2013 gratefully acknowledges the support from the following sponsors: