The 6th International SPIN Workshop on Practical Aspects of Model Checking

Toulouse, France, 21 and 24 September 1999

Co-located with the World Congress on Formal Methods - FM'99

Tuesday, September 21, 1999

Session 1: Keynote Address

10:30 - 11:30 Formal Methods Adoption: What's working, What's not! (PDF)
                 Dan Craigen, ORA Canada, Canada

Session 2: Methodology

11:30 - 12:00 Model Checking for Managers. (PDF)
                 Wil Janssen (Telematica Instituut, The Netherlands),
                 Radu Mateescu (INRIA Rhones-Alpes, France),
                 Sjouke Mauw (Eindhoven University of Technology and CWI, The
                 Peter Fennema, (Telematica Instituut, The Netherlands),
                 Petra van der Stappen (Telematica Instituut, The Netherlands)

12:00 - 12:30 Xspin/Project - Integrated Validation Management for Xspin (PDF)
                 Theo C. Ruys (University of Twente, The Netherlands)

Session 3: Applications I

14:00 - 14:30 Analyzing Mode Confusion Via Model Checking (PDF)
                 Gerald Luettgen, Victor Carreno (NASA Langley Research Center,

14:30 - 15:00 Detecting Feature Interactions in the Terrestrial Trunked Radio (PDF)
              (TETRA) Network
                 Carl B. Adekunle, Steve Schneider (University of London, UK)

15:00 - 15:30 Tool Presentations:

15:00 - 15:15 JAVA PathFinder (PDF)
                 Klaus Havelund (NASA Ames Research Center, USA)

15:15 - 15:30 VIP: A Visual Interface for Promela (PDF)
                 Moataz Kamel, Stefan Leue (University of Waterloo, Canada)

Session 4: Specification and Validation

16:00 - 16:30 Events in Property Patterns (PDF)
                 Marsha Chechik, Dimitrie O. Paun (University of Toronto,

16:30 - 17:00 Assume-Guarantee Model Checking of Software: A Comparative Case (PDF)
                 Corina S. Pasareanu, Matthew B. Dwyer, Michael Huth (Kansas
                 State University, USA)

17:00 - 17:30 A Framework for Automatic Construction of Abstract Promela Models (PDF)
                 Maria-del-Mar Gallardo, Pedro Merino (University of Malaga, Spain)

Friday, September 24, 1999

Session 5: Applications II

10:30 - 11:30 Invited Tutorial: Software Model Checking
              Extracting Spin Models from C Source Code ( sorry, no pdf )
                 Gerard Holzmann, Bell Labs, USA

11:30 - 12:00 Model Checking Operator Procedures (PDF)
                 Wenhui Zhang (Institute for Energy Technology, Norway)

12:00 - 12:30 Applying Model Checking in JAVA Verification (PDF)
                 Klaus Havelund (NASA Ames Research Center, USA),
                 Jens Ulrik Skakkebaek (Stanford University, USA)

Session 6: Extensions

14:00 - 14:30 The Engineering of a Model Checker: Gnu i-Protocol Case Study (PDF)
                 Gerard J. Holzmann (Bell Laboratories, USA)

14:30 - 15:00 Embedding a Dialect of SDL in PROMELA (PDF)
                 Heikki Tuominen (Nokia Telecommunications, Finland)

15:00 - 15:30 dSPIN: A Dynamic Extension of SPIN (PDF)
                 Claudio Demartini, Radu Iosif,
                 Riccardo Sisto (Politecnico di Torino, Italy)