Proceedings of the 8th SPIN Workshop
Toronto, Canada
Held: May 19 - 20, 2001
Published as:
Lecture Notes in Computer Science,
Volume 2057, Springer Verlag.
May 2001, ISSN 0302-9743.
The page numbers below refer to this publication.
Invited talks:
Invited Industrial Presentations:
- Leszek Holenderski (Philips Research)
A model checking project at Philips Research.
- Darren Cofer, Eric Engstrom, Robert Goldman, David Musliner (Honeywell Laboratories)
Applications of model checking at Honeywell Laboratories.
- Bernhard Steffen, Tiziana Margaria, Volker Braun (Metaframe Technologies)
Coarse-grained model checking in practice.
Technical Program:
-
Model checking infinite state-space systems with fine-grained abstractions using Spin.
Marsha Chechik, Benet Devereux, and Arie Gurfinkel, University of Toronto, Canada.
(pp. 16-36, PDF)
- Implementing LTL model checking with net unfoldings,
Javier Esparza, Technical Univiversity Munchen, Germany, and Keiji Heljanko, Helsinki University, Finland.
(pp. 37-56, PDF)
- Directed explicit model checking with HSF-Spin,
Stefan Edelkamp, Alberto Lluch Lafuente, and Stefan Leue, Albert-Ludwig University, Germany.
(pp. 57-79, PDF)
- Addressing dynamic issues of program model checking,
Favio Lerda, and Willem Visser, NASA Ames Research Center, USA.
(pp. 80-102, PDF)
- Automatically validating temporal safety properties of interfaces,
Thomas Ball, and Sriram K. Rajamani, Microsoft Research, Seattle, USA.
(pp. 103-122, PDF)
- Verification experiments on the MASCARA protocol,
Guoping Jia, and Susanne Graf, Verimag, Grenoble, France.
(pp. 123-142, PDF)
- Using Spin for feature interaction analysis - a case study,
Muffy Calder and Alice Miller, University of Glasgow, UK.
(pp. 143-162, PDF)
- Behavioral analysis of the Enterprise JavaBeans(tm) component architecture
Shin Nakajima, NEC Corporation, Japan, and Tesuo Tamai, University of Tokyo, Japan.
(pp. 163-182, PDF)
- p2b: A translation utility for linking Promela and symbolic model checking,
Michael Baldamus, Jochen Schroder-Babo, University of Karlsruhe, Germany.
(pp. 183-191, PDF)
- Transformations for model checking distributed Java programs,
Scott D. Stoller, Yanhong A. Liu, SUNY at Stony Brook, USA.
(pp. 192-199, PDF)
- Distributed LTL model checking in Spin,
Jiri Barnat, Lubos Brim, Masaryk University Brno, and Jitka Stribrna, University of Pennsylvania, USA.
(pp. 200-216, PDF)
- Parallel state space construction for model checking,
Hubert Garavel, Radu Mateescu, and Irina Smarundache, INRIA, Rhone-Alpes, France.
(pp. 217-234, PDF)
- Model checking systems of replicated processes with Spin,
Fabrice Derapas, Nortel Networks, and Pauls Gastin, (University of Paris, France.
(pp. 235-251, PDF)
- A Spin-based model checker for telecommunications protocols,
Vivek K. Shanbhag, and K. Gopinath, Indian Institute of Science, Bangalore, India.
(pp. 252-271, PDF)
- Modeling and verifying a price model for congestion control in computer networks using Promela/Spin,
Clement Yuen, and Wei Tjioe, University of Toronto, Canada.
(pp. 272-287, PDF)
Program committee:
- George Avrunin (University of Massachusetts, USA)
- Thomas Ball (Microsoft Research, USA)
- Ed Brinksma (University of Twente, The Netherlands)
- Marsha Chechik (University of Toronto, Canada)
- Dennis R. Dams (Eindhoven University, The Netherlands)
- Klaus Havelund (NASA Ames Research Center, USA)
- Connie Heitmeier (Naval Research Laboratory, USA)
- Gerard J. Holzmann (Bell Laboratories, USA)
- Fabio Somenzi (University of Colorado, USA)
- Willem Visser (NASA Ames Research Center, USA)
- Pierre Wolper (Universite de Liege, Belgium)
Spin2001 Workshop organization:
- Moshe Y. Vardi (Rice University, USA, general chair)
- Matt B. Dwyer (Kansas State Univesity, USA, program chair)
- Marsha Chechik (University of Toronto, Canada, local arrangements chair)
Spin Homepage
(Page updated: 21 May 2001)