SPIN 2004
11th International SPIN Workshop on Model Checking
of Software
April 1-3, 2004, Barcelona, Spain
Call for Papers
[SPIN 2004 Home Page] [Organizers
and Committees] [Submission Web Site]
[SPIN Policies] [History of SPIN Workshops] [The SPIN Tool Page]
Theme: Validation of software systems
The SPIN workshop is a forum for practitioners and researchers interested
in model checking based techniques for the validation and analysis of communication
protocols and software systems. Techniques 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 symbolic
representations, is the focus of this workshop. It has proven to be particularly
suitable to analyze concurrent asynchronous systems. The workshop will focus
on topics including theoretical and algorithmic foundations and tools, model
derivation from code and code derivation from models, techniques for dealing
with large and infinite state spaces, timing and applications. The workshop
aims to encourage interactions and exchanges of ideas with all related areas
in software engineering.
Solicited Contributions
SPIN 2004 solicits
previously unpublished, currently unsubmitted, original contributions addressing
theoretical, experimental and applied problems in model checking of software
artifacts. Particular topics include:
- model checking based
tools, tool extensions and comparative studies
- theoretical and
algorithmic foundations of model checking based analysis
- combination of model-checking
techniques with other analysis techniques
- model checking of
programming languages and code analysis
- techniques for analyzing
and testing large and infinite state systems
- model checking in
the system life-cycle
- innovative applications
of model checking, including
- model checking of
object-oriented and component based systems
- model checking of
security systems
- model checking of
real-time systems
- engineering of model
checking tools and platforms
- convincing case
study which apply model-checking to real software systems
Submitted papers may
not necessarily focus on tools and model checking approaches based on explicit
state space representations as they are used in SPIN and other tools. Nevertheless,
unless obvious from the paper, it is expected that authors show the relationship
of their work to explicit-state model checking, possibly by showing how
the results could be applied to the SPIN tool or one of the other relevant
explicit state space validation tools.
We solicit submissions
of three categories:
Full papers:
submissions are limited to 18 pages, and should adhere to Springer Verlag's
LNCS format,
preferably using LaTeX. The format of the submissions should be either pdf
or postscript.
Tool presentations:
SPIN 2004 solicits proposals for the demonstration of tools pertinent to
the technical objective of this workshop. Proposals should be submitted as
a summary of up to 5 pages (using Springer Verlag's LNCS format) which
will be included in the workshop proceedings. The title of the summary should
clearly indicate that this is a tool demonstration summary. Longer tool-related
contributions should be submitted as technical papers.
Tutorials: SPIN
2004 solicits proposals for introductory, advanced and industrial application
tutorials on all topics pertinent to the technical objective of this workshop.
Tutorial proposals should detail intended contents, audience and presentation
length. A one-page abstract of accepted tutorials will be included in the
workshop proceedings.
Accepted contributions
will be included in the workshop proceedings which will be published by
Springer Verlag in the Lecture
Notes in Computer Science series. Authors of selected papers may be invited
to submit an expanded version of their work in a special section of the
International Journal
on Software Tools for Technology Transfer (STTT).
Submission and Deadlines
Submission deadlines (firm):
December, 6, 2003: abstracts
December, 14, 2003: complete submission
For submission of technical papers or tool demonstrations use the web site at URL
http://sttt.cs.uni-dortmund.de/spin04/servlet/Conference,
For tutorials, or in case of problems or questions, contact
Laurent Mounier and Susanne Graf
Notification of acceptance: January 18, 2004
Final versions due: February 1, 2004
Workshop date: April 1-3, 2004
Programme Committee
Susanne Graf (Verimag,
Grenoble, F, chair)
Laurent Mounier
(Verimag, Grenoble, F, chair)
Bernard Boigelot
(Liège, B)
Dragan Bosnacki (Eindhoven,
NL)
David Dill (Stanford,
USA)
Javier
Esparza (Stuttgart, D)
Patrice Godefroid
(Bell Laboratories, USA)
John Hatcliff (Kansas
State, USA),
|
Gerard Holzmann
(Bell Labs, USA),
Stefan Leue
(Freiburg, D)
Pedro Merino (Málaga,
E)
Mooly Sagiv (Tel-Aviv,
Il)
Scott Stoller
(Stony Brook, USA)
Antti Valmari
(Tampere, Finnland)
|
Advisory Committee:
Gerard Holzmann
(chair), Amir Pnueli
Steering Committee:
Thomas Ball,
Susanne Graf,
Stefan Leue,
Moshe Vardi, Pierre Wolper (chair)
[Susanne Graf] April, 2003
spin04@imag.fr