*******************************************************
                  Call for Papers: SPIN 2011
    18th Int. SPIN Workshop on Model Checking of Software
            July 14-15, Snowbird, Utah, USA
		Co-located with CAV 2011

   *******************************************************

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:          1 April 2011
Notification of acceptance/rejection:            13 May 2011
Deadline for final version of accepted papers:   3 June 2011
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 compositionnality
- 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.  No
longer than 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.


Organization
------------
Program Chairs:
Alex Groce (Oregon State University, Corvallis)
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 (Verimag)
Aarti Gupta (NEC Labs, USA)
Klaus Havelund (Jet Propulsion Laboratory, Pasadena)
Gerard Holzmann (Jet Propulsion Laboratory, Pasadena)
Gerwin Klein (NICTA, 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)
David Parker (University of Oxford)
Corina Pasareanu (Carnegie Mellon University/NASA Ames)
Doron Peled (Bar Ilan University)
Koushik Sen (University of California, Berkeley)
Scott Stoller (Stony Brook University)
Murali Talupur (SCL, Intel)