Aim and Scope:

The SPIN workshop is a forum for practitioners and researchers interested in state space-based techniques for the validation and analysis of software systems. Theoretical techniques and empirical evaluations based on explicit representations of state spaces, as implemented in the SPIN model checker or other tools, or techniques based on combination of explicit representations with other representations, are the focus of this workshop.


We particularly welcome papers describing the development and application of state space exploration techniques in testing and verifying embedded software, security-critical software, enterprise and web applications, and other interesting software platforms. The workshop aims to encourage interactions and exchanges of ideas with all related areas in software engineering.


Important Dates and Deadlines:

Deadline for submission of full papers: (Now Closed) April 15 AoE

Notification of acceptance/rejection: (Now Closed) May 6

Deadline for final version of accepted papers: (Now Closed) May 13

Workshop: July 14-15


Topics of Interest:

-          Algorithms and storage methods for explicit state model checking

-          Automated testing using model checking techniques

-          Derivation of invariants, test cases, or other useful information from state spaces

-          Abstraction and the use of static analysis to reduce state spaces

-          Model checking of programming languages and code analysis

-          Directed model checking using heuristics

-          Parallel or distributed model checking using multi-core or multiple computers

-          Techniques for dealing with infinite state spaces

-          Model checking of timed and probabilistic systems

-          Combinations of enumerative and symbolic techniques

-          Analysis for modeling languages, including SE languages (UML,...)

-          New property specification languages, including new forms of temporal logic

-          Combination of model-checking techniques with other analysis techniques

-          Modularity and compositionality

-          Comparative studies, including to other model checking techniques

-          Case studies of interesting systems or with interesting results

-          Theoretical and algorithmic foundations of model-checking based analysis

-          Engineering and implementation of model-checking tools and platforms

-          Insightful surveys or historical accounts on topics of relevance to SPIN workshops


Solicited Contributions:


With the exception of survey and history papers, the papers should contain original work which has not been submitted or accepted for publication elsewhere. Submissions should adhere to the LNCS format. We solicit two kinds of papers:

1.      Technical Papers: At most 18 pages in LNCS format. All accepted technical papers will be included in the proceedings.

2.      Tool Presentations: This kind of submission should consist of two parts: the first part is at most a 5 page description of the tool. If accepted, this part will be published in the workshop proceedings. The second part should describe an informal plan for an oral presentation of the tool. This part will not be included in the proceedings.

The proceedings of SPIN usually appear in Springer's Lecture Notes in Computer Science series. We are confident we will continue this tradition for the 2011 edition.


Submission Site:

Please submit your papers via the paper submission website.



Program Chairs:

Alex Groce

Oregon State University, USA

Madanlal Musuvathi

Microsoft Research, Redmond


Program Committee:

James Andrews

University of Western Ontario, London, Canada

Dragan Bosnacki

Eindhoven University of Technology

Sebastian Burckhardt

Microsoft Research, Redmond

Cristian Cadar

Imperial College, London

George Candea

EPFL, Switzerland

Sagar Chaki

Software Engineering Institute, Pittsburgh

Supratik Chakraborty

I.I.T. Bombay, India

Azadeh Farzan

University of Toronto, Canada

Susanne Graf


Alex Groce

Oregon State University, USA

Aarti Gupta


Klaus Havelund

Jet Propulsion Laboratory, Pasadena

Gerard Holzmann

Jet Propulsion Laboratory, Pasadena

Gerwin Klein

NICTA & UNSW, Sydney

Akash Lal

Microsoft Research, India

Alberto Lluch Lafuente

IMT Institute for Advanced Studies, Lucca

Rupak Majumdar

Max Planck Institute for Software Systems

Darko Marinov

University of Illinois, Urbana-Champaign

Madanlal Musuvathi

Microsoft Research, Redmond

David Parker

University of Oxford

Corina Pasareanu

Carnegie Mellon/NASA Ames

Doron Peled

Bar Ilan University

Koushik Sen

University of California, Berkeley

Scott Stoller

Stony Brook University

Murali Talupur

SCL, Intel