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
Netherlands),
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,
USA)
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,
Canada)
16:30 - 17:00 Assume-Guarantee Model Checking of Software: A Comparative
Case (PDF)
Study
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)
Revisited
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)