Call for papers

22th International Symposium on Model Checking Software – SPIN
24–26 August, Stellenbosch, South Africa

Important Dates

  • Submission of abstracts: 17 April (Anywhere on Earth)
  • Submission of full papers: 4 May (Anywhere on Earth)
  • Notification of acceptance/rejection: 15 June
  • Final version due: 29 June
  • Symposium: 24–26 August

Aims and Scope

The SPIN Symposium 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 symposium.

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

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:

LNCS Information for Authors

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 ideas and work in progress.
  • 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.

Papers should be submitted via the

Easy Chair SPIN submission website.

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

Programme Chairs

  • Bernd Fischer (Stellenbosch University)
  • Jaco Geldenhuys (Stellenbosch University)

Programme Committee

  • Christel Baier (Technical University of Dresden)
  • Dragan Bosnacki (Eindhoven University of Technology)
  • Sagar Chaki (Carnegie Mellon Software Engineering Institute)
  • Alessandro Cimatti (FBK-irst)
  • Lucas Cordeiro (Federal University of Amazonas)
  • Alexandre Duret-Lutz (LRDE/EPITA)
  • Matt Dwyer (University of Nebraska)
  • Susanne Graf (Universite Joseph Fourier / CNRS / VERIMAG)
  • Alex Groce (Oregon State University)
  • Klaus Havelund (Jet Propulsion Laboratory, California Institute of Technology)
  • Gerard Holzmann (NASA/JPL)
  • Franjo Ivancic (Google)
  • Sarfraz Khurshid (The University of Texas at Austin)
  • Shuvendu Lahiri (Microsoft Research)
  • Stefan Leue (University of Konstanz, Department of Computer and Information Science)
  • Igor Melatti (Department of Computer Science, University Of Rome “La Sapienza”)
  • Eric Mercer (Brigham Young University)
  • Gennaro Parlato (University of Southampton)
  • Suzette Person (NASA Langley Research Center)
  • Stefan Schwoon (ENS de Cachan / INRIA)
  • Jaco Van De Pol (University of Twente)
  • Helmut Veith (Vienna University of Technology)

Steering Committee

  • Dragan Bosnacki (Eindhoven University of Technology, Netherlands)
  • Susanne Graf (CNRS/VERIMAG, France)
  • Gerard Holzmann (chair) (NASA/JPL, USA)
  • Stefan Leue (University of Konstanz, Germany)
  • Willem Visser (Stellenbosch University, South Africa)