Logic List Mailing Archive

SPIN Workshop on Model Checking of Software

27-29 Sep 2010
Twente, The Netherlands

17th International SPIN Workshop on Model Checking of Software

September 27--29, 2010, University of Twente, The Netherlands
URL: <http://www.utwente.nl/spin2010/>
Co-located with:
ICGT 2010 <http://www.utwente.nl/icgt-spin/>,=20
PDMC+HiBi 2010, <http://pdmc.cz/PDMC10/>

NEWS
=3D=3D=3D=3D
Invited speakers are confirmed:

* Javier Esparza, Technical University of Munich, Germany
(joint keynote speaker with ICGT 2010)
* Alessandro Cimatti, FBK-IRST, Italy
* Darren Cofer, Rockwell Collins, USA


Aim and Scope
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

The SPIN workshop is a forum for practitioners and researchers
interested in state space-based techniques for the validation and
analysis of software systems. The focus of the workshop is on
theoretical advances and empirical evaluations based on explicit
representations of state spaces, as implemented in the SPIN model
checker or other tools, or techniques based on combinations of
explicit and other symbolic representations. We welcome papers
describing the development and application of state-space and
path-exploration techniques for the testing and the verification of
security-critical software, enterprise and web applications, embedded
software, 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):
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D

* Algorithms and storage methods for explicit-state model checking
* Theoretical and algorithmic foundations of model-checking based =
analysis
* Directed model checking using heuristics
* Parallel or distributed model checking
* Model checking of timed and probabilistic systems
* Abstraction and symbolic execution techniques in relation to software =
verification
* Static analysis for state space reduction
* Combinations of enumerative and symbolic techniques
* Analysis for modeling languages, such as UML/state charts
* Property specification languages, including new forms of temporal =
logic
* Model checking for various programming languages and code analysis
* Automated testing using state space and/or path exploration techniques
* Derivation of specifications, test cases, or other useful material =
from state spaces
* Combination of model-checking techniques with other analysis =
techniques
* Modularity and compositionality
* Comparative studies, including comparisons with other model-checking =
techniques
* Case studies of interesting systems or with interesting results
* Engineering and implementation of model-checking tools and platforms
* Benchmarks for software verification


Solicited Contributions
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

We solicit two kinds of papers:

* TECHNICAL PAPERS. These papers should contain original work which
has not been submitted or accepted for publication elsewhere.
Submissions should adhere to the LNCS format and should be no
longer than 18 pages.

* TOOL PAPERS. These papers should describe novel tools or tool
extensions. If previous versions of the described tool have been
published before, the novel features of the tool should be
explained clearly. These papers should also specify availability
of the tool, number of users, and applications/case studies. Tool
paper submissions should consist of two parts. The first part is
at most 5 pages in LNCS format. The name "Tool Presentation"
should appear in the title. If accepted, this 5 page paper will be
published in the workshop proceedings. The second part should
describe an informal plan for the oral presentation of the tool.
This part will not be included in the proceedings.

If accepted, both regular and tool papers will be presented at the
conference and will be included in the workshop proceedings. At
least one author of each accepted paper is expected to be present
at the conference. Submissions are held confidential until publication.


Submission and Publication
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D

As in previous years, the proceedings of this edition of the workshop
will appear in Lecture Notes in Computer Science.


Important Dates
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

Abstract submission: April 9, 2010
Paper submission: April 16, 2010
Notification of acceptance: June 7, 2010
Final papers due: June 28, 2010
Workshop: September 27--29, 2010


ORGANIZATION
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

Program Chairs:

Jaco van de Pol, U Twente, Netherlands
Michael Weber, U Twente, Netherlands

Program Committee:

Dragan Bosnacki (TU Eindhoven, The Netherlands)
Jiri Barnat (Masaryk University Brno, Czech Republic)
Stefan Edelkamp (University of Bremen, Germany)
Patrice Godefroid (Microsoft Research, Redmond, USA)
Ganesh Gopalakrishnan (University of Utah, USA)
Jan Friso Groote (TU Eindhoven, The Netherlands)
Orna Grumberg (Technion, Israel)
Gerard Holzmann (NASA/JPL, USA)
Radu Iosif (Verimag Grenoble, France)
Stefan Leue (University of Konstanz, Germany)
Rupak Majumdar (University of California at Berkeley, USA)
Eric G. Mercer (Brigham Young University, USA)
Albert Nymeyer (University of New South Wales, Australia)
Dave Parker (Oxford Univerisity, UK)
Corina Pasareanu (CMU/NASA Ames, USA)
Doron Peled (Bar-Ilan University, Israel)
Paul Pettersson (Malardalen University, Sweden)
Scott Stoller (Stony Brook University, USA)
Willem Visser (Stellenbosch University, South Africa)
Tomohiro Yoneda (National Institute of Informatics, Japan)

Steering Committee:

Susanne Graf, VERIMAG, France
Gerard Holzmann, JPL, USA
Stefan Leue (chair), U Konstanz, Germany
Pierre Wolper, U Liege, Belgium

--=20
Michael Weber
University of Twente, The Netherlands
http://fmt.cs.utwente.nl/~michaelw/