SPIN 2016
23rd International SPIN Symposium on Model Checking of Software
7--8 April 2016, Eindhoven, The Netherlands
http://www.spin2016.info
(colocated with ETAPS 2016)
======================================================================
---- Important Dates ----
Submission of papers: 8 January 2016 (Anywhere on Earth)
Notification of acceptance/rejection: 12 February 2016
Final version due: 24 February 2016
Symposium: 7--8 April 2016
---- Aims and Scope ----
The 23rd edition of the SPIN symposium aims at bringing together
practitioners and researchers interested in symbolic and state
space-based techniques for the validation and analysis of software
systems. 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 symposium.
We particularly welcome papers describing the development and
application of state space exploration techniques in testing and
verifying embedded software, safety-critical software, enterprise
and web applications, and other interesting software platforms. The
symposium 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 symposium
SPIN 2016 will be colocated with the 19th European Joint Conferences on
Theory and Practice of Software (ETAPS 2016). An overview of the previous
SPIN symposia can be found at http://spinroot.com/spin/Workshops.
---- Paper Submission and Publication ----
The proceedings of SPIN will be published in Springer's Lecture Notes in
Computer Science series. A selection of papers will be invited to a special
issue of the International Journal on Software Tools for Technology Transfer
(STTT).
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. All accepted technical papers will be
included in the proceedings.
- Idea Papers:
At most 6 pages in LNCS format that describe novel
research directions in software model checking. New idea
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. If accepted, this part
will be published in the symposium 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 and may
also be in the form of a five minute video. Tools must be
available online for reviewers to inspect.
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 symposium
and present the paper.
---- Organisation ----
Program Chairs
- Dragan Bosnacki (Eindhoven University of Technology)
- Anton Wijs (Eindhoven University of Technology)
Program Committee
Erika Abraham (RWTH Aachen University, GER)
Jiri Barnat (Masaryk University, CZE)
Aleksandar Dimovski (IT University of Copenhagen, DEN)
Stefan Edelkamp (University of Bremen, GER)
Bernd Fischer (Stellenbosch University, RSA)
Jaco Geldenhuys (Stellenbosch University, RSA)
Alex Groce (Oregon State University, USA)
Jan Friso Groote (Eindhoven University of Technology, NED)
Gerard Holzmann (NASA / Jet Propulsion Laboratory, USA)
Franjo Ivancic (Google, USA)
Alfons Laarman (Vienna University of Technology, AUT)
Stefan Leue (University of Konstanz, GER)
Alberto Lluch Lafuente (Technical University of Denmark, DEN)
Radu Mateescu (INRIA Rhone-Alpes, FRA)
Eric Mercer (Brigham Young University, USA)
Pedro Merino (University of Malaga, ESP)
Alice Miller (University of Glasgow, UK)
Jun Pang (University of Luxembourg, LUX)
Corina Pasareanu (NASA Ames / Carnegy Mellon University, USA)
Theo Ruys (RUwise, NED)
Jun Sun (Singapore University of Technology and Design, SIN)
Michael Tautschnig (Queen Mary University, UK)
Mohammad Torabi Dashti (ETH Zuerich, SUI)
Martin Wehrle (University of Basel, SUI)
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
