SPIN Programme

Programme of SPIN 2004

All SPIN sessions will be in the "sala actes", in the B6 building.

THURSDAY, April 1

9.00
10.00 TACAS Invited Talk
Antti Valmari (Tampere University of Technology, SF)
What the Small Rubik's Cube Taught Me on Data Structures, Information Theory and Randomisation
Session chair:

10.00
10.30 Coffee

10.30
10.40
SPIN Opening

10.30
12.30 Session 1: Heuristics and Probabilities

Session chair: S. Leue

Typical Structural Properties of State Spaces
Radek Pelánek (MU Brno, CZ)

State Caching Reconsidered
Jaco Geldenhuys (Tampere University of Technology, SF)

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

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

12.30
14.30 Lunch + SPIN Steerring Comitee Meeting (Restricted)

14.30
15.30 CC Invited Talk
Mary Lou Soffa (University of Pittsburgh, USA)
Developing a Foundation for Code Optimization
Session chair:

15.30
16.30 Tutorial 1 (part 1)

Advanced SPIN
Theo C. Ruys (University of Twente, NL), Gerard. J. Holzmann (NASA JPL Laboratory, USA)

16.30
17.00 Coffee

17.00
19.00 Tutorial 1 (part 2)

Advanced SPIN
Theo C. Ruys (University of Twente, NL), Gerard. J. Holzmann (NASA JPL Laboratory, USA)

19.00
19.30 SPIN Business Meeting (Public)

Evening
eTX Reception (ETAPS)

FRIDAY, April 2

9.00
10.00 ETAPS Invited Talk
Robin Milner (Cambridge University, UK)
A Grand Challenge: Theories for Global Ubiquitous Computing
Session chair:

10.00
10.30 Coffee

10.30
11.30 Session 2: Improvments of SPIN

Session chair: J. Hatcliff

Model-Driven Software Verification
Gerard Holzmann, Rajeev Joshi (NASA JPL Laboratory, USA)

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

10.30
11.30
Session 3: Validation of Timed Systems

Session chair: S. Stoller

Black-box conformance testing for real-time systems
Moez Krichen, Stavros Tripakis (Verimag Grenoble, F)

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

12.30
14.30 Lunch

14.30
15.30 Session 4: Tool papers (20 minutes per presentation)

Session chair: L. Mounier

Hopper: A tool for exploring explicit model checking algorithms
Michael Jones, Eric Mercer (Brigham Young University, USA)

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

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

15.30
16.30
Tutorial 2 (part 1)

The IF validation environment
Marius Bozga, Laurent Mounier, Iulian Ober (Verimag Grenoble, F)

16.30
17.00 Coffee

17.00
19.00 Tutorial 2 (part 2)

The IF validation environment
Marius Bozga, Laurent Mounier, Iulian Ober (Verimag Grenoble, F)

21.00 SPIN Dinner

SATURDAY, April 3

9.00
10.00
SPIN Invited Talk
Reinhard Wilhelm (University of Saarbrucken, G)
Formal Analysis of Processor Timing Models
Session chair: S. Graf

10.00
10.30
Coffee

10.30
12.30
Session 5: Abstraction and symbolic methods

Session chair: B. Boigelot

Verification of Java Programs using Symbolic Execution and Invariant Generation
Corina Pasareanu, Willem Visser (NASA Ames Research Center, USA)

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

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

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

12.30
14.00
Lunch

14.00
16.00
Session 6: Applications

Session chair: D. Bosnacki

Translation from Adapted UML to Promela for CORBA-based Applications
Jessica Chen, Hanmei Cui (University of Windsor, CA)

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

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

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

16.00
16.10
Closing Session

16.10
16.30
Coffee

THURSDAY, April 1
9.00 10.00	TACAS Invited Talk Antti Valmari (Tampere University of Technology, SF) What the Small Rubik's Cube Taught Me on Data Structures, Information Theory and Randomisation Session chair:
10.00 10.30	Coffee
10.30 10.40	SPIN Opening
10.30 12.30	Session 1: Heuristics and Probabilities Session chair: S. Leue Typical Structural Properties of State Spaces Radek Pelánek (MU Brno, CZ) State Caching Reconsidered Jaco Geldenhuys (Tampere University of Technology, SF) Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM Peter Leven (University of Freiburg, G) , Tilman Mehler, Stefan Edelkamp (University of Dortmund, G) Fast and* Accurate Bitstate Verification for SPIN* Peter Dillinger, Panagiotis Manolios (Georgia Institute of Technology, USA)
12.30 14.30	Lunch + SPIN Steerring Comitee Meeting (Restricted)
14.30 15.30	CC Invited Talk Mary Lou Soffa (University of Pittsburgh, USA) Developing a Foundation for Code Optimization Session chair:
15.30 16.30	Tutorial 1 (part 1) Advanced SPIN Theo C. Ruys (University of Twente, NL), Gerard. J. Holzmann (NASA JPL Laboratory, USA)
16.30 17.00	Coffee
17.00 19.00	Tutorial 1 (part 2) Advanced SPIN Theo C. Ruys (University of Twente, NL), Gerard. J. Holzmann (NASA JPL Laboratory, USA)
19.00 19.30	SPIN Business Meeting (Public)
Evening	eTX Reception (ETAPS)
FRIDAY, April 2
9.00 10.00	ETAPS Invited Talk Robin Milner (Cambridge University, UK) A Grand Challenge: Theories for Global Ubiquitous Computing Session chair:
10.00 10.30	Coffee
10.30 11.30	Session 2: Improvments of SPIN Session chair: J. Hatcliff Model-Driven Software Verification Gerard Holzmann, Rajeev Joshi (NASA JPL Laboratory, USA) Minimization of counter-examples in SPIN Paul Gastin, Pierre Moro, Marc Zeitoun (LIAFA Paris 7, F)
10.30 11.30	Session 3: Validation of Timed Systems Session chair: S. Stoller Black-box conformance testing for real-time systems Moez Krichen, Stavros Tripakis (Verimag Grenoble, F) Model checking of UML models via a mapping to communicating extended timed automata Iulian Ober, Susanne Graf, Ileana Ober (Verimag Grenoble, F)
12.30 14.30	Lunch
14.30 15.30	Session 4: Tool papers (20 minutes per presentation) Session chair: L. Mounier Hopper: A tool for exploring explicit model checking algorithms Michael Jones, Eric Mercer (Brigham Young University, USA) SEQ.OPEN: A Tool for Efficient Trace-Based Verification Radu Mateescu, Hubert Garavel (INRIA Rhone-Alpes, F) Model Checking Genetic Regulatory Networks using GNA and CADP Gregory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu (INRIA Rhone-Alpes, F)
15.30 16.30	Tutorial 2 (part 1) The IF validation environment Marius Bozga, Laurent Mounier, Iulian Ober (Verimag Grenoble, F)
16.30 17.00	Coffee
17.00 19.00	Tutorial 2 (part 2) The IF validation environment Marius Bozga, Laurent Mounier, Iulian Ober (Verimag Grenoble, F)
21.00	SPIN Dinner
SATURDAY, April 3
9.00 10.00	SPIN Invited Talk Reinhard Wilhelm (University of Saarbrucken, G) Formal Analysis of Processor Timing Models Session chair: S. Graf
10.00 10.30	Coffee
10.30 12.30	Session 5: Abstraction and symbolic methods Session chair: B. Boigelot Verification of Java Programs using Symbolic Execution and Invariant Generation Corina Pasareanu, Willem Visser (NASA Ames Research Center, USA) Polynomial Time Image Computation With Interval-definable Counters Systems Jerome Leroux, Alain Finkel (LSV Cachan, F) Using Fairness to Make Abstractions Work Natalia Sidorova, Dragan Bosnacki (Eindhoven University of Technology, NL), Natalia Ioustinova (CWI, NL) A Scalable Incomplete Test for Message Buffer Overflow in Promela Models Wei Wei, Stefan Leue, Richard Mayr (University of Freiburg, G)
12.30 14.00	Lunch
14.00 16.00	Session 6: Applications Session chair: D. Bosnacki Translation from Adapted UML to Promela for CORBA-based Applications Jessica Chen, Hanmei Cui (University of Windsor, CA) Verifying Commit-Atomicity using Model-Checking Cormac Flanagan (University of California at Santa Cruz, USA) Analysis of Distributed Spin Applied to Industrial-Scale Model Murali Rangarajan, Samar Dajani-Brown, Kirk Schloegel, Darren Cofer (Honeywell Laboratories, USA) Verification of MPI-Based Software for Scientific Computation Stephen Siegel, George S. Avrunin (University of Massachusetts, USA)
16.00 16.10	Closing Session
16.10 16.30	Coffee