`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:
Applications 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)

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

`Technical Program:`

`Organizing Committee`

`Program Committee`

`Advisory Committee`

`Steering Committee`

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: Applications	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)