======================================================================
SPIN 2015

22nd International Workshop on Model Checking Software
24--26 August 2015, Stellenbosch, South Africa
http://www.spin2015.org
======================================================================

---- Important Dates ----

Submission of abstracts: 17 April 2015 (Anywhere on Earth)
Submission of full papers: 24 April 2015 (Anywhere on Earth)
Notification of acceptance/rejection: 15 June 2015
Final version due: 29 June 2015
Workshop: 24--26 August 2015

---- Aims and Scope ----

The SPIN workshop is a forum for practitioners and researchers
interested in symbolic and 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 the 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. Topics of interest
include, but are not limited to:

- Formal verification techniques for automated analysis of software
- Algorithms and storage methods for explicit-state model checking
- Theoretical and algorithmic foundations of model checking
- Model checking for programming languages and code analysis
- Directed model checking using heuristics
- Parallel or distributed model checking
- Verification of timed and probabilistic systems
- Model checking techniques for biological systems
- Formal verification techniques for concurrent software
- Formal verification techniques for embedded software
- Abstraction and symbolic execution techniques in relation to
software verification
- Static analysis for state space reduction
- Combinations of enumerative and symbolic techniques
- Analysis for modelling languages, such as UML/state charts
- Property specification languages, including temporal logics
- Automated testing using state space and/or path exploration
- Derivation of specifications, test cases, or other useful material
from state spaces
- Combination of model checking techniques with other analyses
- Modular and compositional verification techniques
- Case studies of interesting systems or with interesting results
- Engineering and implementation of software verification tools
- Benchmark and comparative studies for formal verification tools
- Insightful surveys or historical accounts on topics of relevance to
the workshop

---- Paper Submission and Publication ----

The proceedings of SPIN will be published in Springer-Verlag's
Lecture Notes in Computer Science series. 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:

http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0

We solicit three kinds of papers:

- Technical Research Papers:
At most 18 pages in LNCS format.

- Idea Papers:
At most 6 pages in LNCS format that describe describe novel
research directions in software model checking. New ideas
submissions are intended to describe well-defined research ideas
that are at an early stage of investigation and may not be fully
validated.

- Tool Presentations:
This kind of submission should consist of two parts: the first part
is at most a 6-page description of the tool. The second part
should describe an informal plan for an oral presentation of the
tool. This part will not be included in the proceedings and may
also be in the form of a five minute video. Tools must be
available online for reviewers to inspect.

Papers should be submitted via Easychair:

https://www.easychair.org/conferences/?conf=spin20150

All papers that conform to submission guidelines will be
peer-reviewed by members of the program committee. Submissions will
be evaluated on the basis of originality, importance of contribution,
soundness, evaluation, quality of presentation, and appropriate
comparison to related work. At least one author of each accepted
paper must attend the workshop and present the paper.

---- Organisation ----

Program Chairs

- Bernd Fischer (Stellenbosch Univ)
- Jaco Geldenhuys (Stellenbosch Univ)

Program Committee

- Christel Baier (Technical Univ of Dresden)
- Dragan Bosnacki (Eindhoven Univ of Tech.)
- Sagar Chaki (Carnegie Mellon Softw. Eng. Inst.)
- Alessandro Cimatti (FBK-irst)
- Lucas Cordeiro (Federal Univ of Amazonas)
- Alexandre Duret-Lutz (LRDE/EPITA)
- Matt Dwyer (Univ of Nebraska)
- Susanne Graf (Univ Joseph Fourier / CNRS / VERIMAG)
- Alex Groce (Oregon State Univ)
- Klaus Havelund (Jet Propulsion Lab., California Inst. of Tech.)
- Gerard Holzmann (NASA/JPL)
- Franjo Ivancic (Google)
- Sarfraz Khurshid (The Univ of Texas at Austin)
- Shuvendu Lahiri (Microsoft Research)
- Stefan Leue (Univ of Konstanz, Dept of Comp. and Information Sci.)
- Igor Melatti (Dept of Comp. Sci., Univ Of Rome "La Sapienza")
- Eric Mercer (Brigham Young Univ)
- Gennaro Parlato (Univ of Southampton)
- Suzette Person (NASA Langley Research Center)
- Stefan Schwoon (ENS de Cachan / INRIA)
- Jaco van de Pol (Univ of Twente)
- Helmut Veith (Vienna Univ of Tech.)