Proceedings of the 11th SPIN Workshop
Barcelona, Spain
Co-located with ETAPS 2004
In cooperation with ACM SIGSOFT
April 1 - 3, 2004

Published as:
	Lecture Notes in Computer Science,
	Volume 2989, Springer Verlag, April 2004

Technical Program:

Session 1
Heuristics and Probabilities
Typical Structural Properties of State Spaces (PDF)
Radek Pelánek (MU Brno, CZ)

State Caching Reconsidered (PDF)
Jaco Geldenhuys (Tampere Univ. of Technology,  SF)

Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM (PDF)
Peter Leven (Univ. of Freiburg, G) , Tilman Mehler, Stefan Edelkamp (Univ. of Dortmund, G)

Fast and Accurate Bitstate Verification for SPIN (PDF)
Peter Dillinger, Panagiotis Manolios (Georgia Institute of Technology, USA)

Tutorial 1
Part 1&2
Advanced SPIN (PDF)
Theo C. Ruys (Univ. of Twente, NL), Gerard. J. Holzmann (NASA/JPL, USA)
Session 2:
Improvments of SPIN
Model-Driven Software Verification (PDF)
Gerard Holzmann, Rajeev Joshi (NASA/JPL, USA)

Minimization of counter-examples in SPIN (PDF)
Paul Gastin, Pierre Moro, Marc Zeitoun (LIAFA Paris 7, F)

Session 3:
Validation of Timed Systems
Black-box conformance testing for real-time systems (PDF)
Moez Krichen, Stavros Tripakis (Verimag Grenoble, F)

Model checking of UML models via a mapping to communicating extended timed automata (PDF)
Iulian Ober, Susanne Graf, Ileana Ober (Verimag Grenoble, F)

Session 4:
Tool papers
Hopper: A tool for exploring explicit model checking algorithms (PDF)
Michael Jones, Eric Mercer (Brigham Young Univ., USA)

SEQ.OPEN: A Tool for Efficient Trace-Based Verification (PDF)
Radu Mateescu, Hubert Garavel (INRIA Rhone-Alpes, F)

Model Checking Genetic Regulatory Networks using GNA and CADP (PDF)
Gregory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu (INRIA Rhone-Alpes, F)

Tutorial 2
Part 1&2
The IF validation environment (PDF)
Marius Bozga, Laurent Mounier, Iulian Ober (Verimag Grenoble, F)
Invited Talk Formal Analysis of Processor Timing Models (PDF)
Reinhard Wilhelm (Univ. of Saarbrucken, G)
Session 5
Abstraction and symbolic methods
Verification of Java Programs using Symbolic Execution and Invariant Generation (PDF)
Corina Pasareanu, Willem Visser (NASA Ames Research Center, USA)

Polynomial Time Image Computation With Interval-definable Counters Systems (PDF)
Jerome Leroux, Alain Finkel (LSV Cachan, F)

Using Fairness to Make Abstractions Work (PDF)
Natalia Sidorova, Dragan Bosnacki (Eindhoven Univ. of Technology, NL), Natalia Ioustinova (CWI, NL)

A Scalable Incomplete Test for Message Buffer Overflow in Promela Models (PDF)
Wei Wei, Stefan Leue, Richard Mayr (Univ. of Freiburg, G)

Session 6:
Translation from Adapted UML to Promela for CORBA-based Applications (PDF)
Jessica Chen, Hanmei Cui (Univ. of Windsor, CA)

Verifying Commit-Atomicity using Model-Checking (PDF)
Cormac Flanagan (Univ. of California at Santa Cruz, USA)

Analysis of Distributed Spin Applied to Industrial-Scale Model (PDF)
Murali Rangarajan, Samar Dajani-Brown, Kirk Schloegel, Darren Cofer (Honeywell Laboratories, USA)

Verification of MPI-Based Software for Scientific Computation (PDF)
Stephen Siegel, George S. Avrunin (Univ. of Massachusetts, USA)

Organizing Committee

Susanne Graf (Verimag, Grenoble, F, chair)
Laurent Mounier (Verimag, Grenoble, F, chair)

Program Committee

Bernard Boigelot (Liege, B)
Dragan Bosnacki (Eindhoven, NL)
David Dill (Stanford, USA)
Javier Esparza (Stuttgart, D)
Patrice Godefroid (Bell Laboratories, USA)
Susanne Graf (Verimag, Grenoble, F, chair)
John Hatcliff (Kansas State, USA),
Gerard Holzmann (Pasadena, USA),
Stefan Leue (Freiburg, D)
Pedro Merino (Malaga, E)
Laurent Mounier (Verimag, Grenoble, F)
Mooly Sagiv (Tel-Aviv, Il)
Scott Stoller (Stony Brook, USA)
Antti Valmari (Tampere, Finnland)

Advisory Committee

Gerard Holzmann (NASA/JPL, USA)
Amir Pnueli (Weizman Institute, Il)

Steering Committee

Thomas Ball (Microsoft, USA)
Susanne Graf (Verimag, F)
Stefan Leue (Univ. Freiburg, G)
Moshe Vardi (Rice Univ, USA)
Pierre Wolper (Univ Liege, B)

Spin Homepage
(Page updated: 7 April 2004)