8. SPIN 2001: Toronto, Canada

Matthew B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings. Lecture Notes in Computer Science 2057 Springer 2001, ISBN 3-540-42124-6 BibTeX

@proceedings{DBLP:conf/spin/2001,
  editor    = {Matthew B. Dwyer},
  title     = {Model Checking Software, 8th International SPIN Workshop, Toronto,
               Canada, May 19-20, 2001, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2057},
  year      = {2001},
  isbn      = {3-540-42124-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Keynotes

Doron Peled, Lenore D. Zuck:
From Model Checking to a Temporal Proof. 1-14
Electronic Edition (Springer LINK) BibTeX
Rob Gerth:
Model Checking if Your Life Depends on It a View from Intel's Trenches. 15
Electronic Edition (Springer LINK) BibTeX

Technical Papers and Tool Reports

Marsha Chechik, Benet Devereux, Arie Gurfinkel:
Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN. 16-36
Electronic Edition (Springer LINK) BibTeX
Javier Esparza, Keijo Heljanko:
Implementing LTL Model Checking with Net Unfoldings. 37-56
Electronic Edition (Springer LINK) BibTeX
Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Leue:
Directed Explicit Model Checking with HSF-SPIN. 57-79
Electronic Edition (Springer LINK) BibTeX
Flavio Lerda, Willem Visser:
Addressing Dynamic Issues of Program Model Checking. 80-102
Electronic Edition (Springer LINK) BibTeX
Thomas Ball, Sriram K. Rajamani:
Automatically Validating Temporal Safety Properties of Interfaces. 103-122
Electronic Edition (Springer LINK) BibTeX
Guoping Jia, Susanne Graf:
Verification Experiments on the MASCARA Protocol. 123-142
Electronic Edition (Springer LINK) BibTeX
Muffy Calder, Alice Miller:
Using SPIN for Feature Interaction Analysis - A Case Study. 143-162
Electronic Edition (Springer LINK) BibTeX
Shin Nakajima, Tetsuo Tamai:
Behavioural Analysis of the Enterprise JavaBeans^TM Component Architecture. 163-182
Electronic Edition (Springer LINK) BibTeX
Michael Baldamus, Jochen Schröder-Babo:
p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper). 183-191
Electronic Edition (Springer LINK) BibTeX
Scott D. Stoller, Yanhong A. Liu:
Transformations for Model Checking Distributed Java Programs. 192-199
Electronic Edition (Springer LINK) BibTeX
Jiri Barnat, Lubos Brim, Jitka Stríbrná:
Distributed LTL Model-Checking in SPIN. 200-216
Electronic Edition (Springer LINK) BibTeX
Hubert Garavel, Radu Mateescu, Irina M. Smarandache:
Parallel State Space Construction for Model-Checking. 217-234
Electronic Edition (Springer LINK) BibTeX
Fabrice Derepas, Paul Gastin:
Model Checking Systems of Replicated Processes with Spin. 235-251
Electronic Edition (Springer LINK) BibTeX
Vivek K. Shanbhag, K. Gopinath:
A SPIN-Based Model Checker for Telecommunication Protocols. 252-271
Electronic Edition (Springer LINK) BibTeX
Clement Yuen, Wei Tjioe:
Modeling and Verifying a Price Model for Congestion Control in Computer Networks Using Promela/Spin. 272-287
Electronic Edition (Springer LINK) BibTeX

Invited Project Summaries

Leszek Holenderski:
A Model Checking Project at Philips Research. 288-295
Electronic Edition (Springer LINK) BibTeX
Darren D. Cofer, Eric Engstrom, Robert P. Goldman, David J. Musliner, Steve Vestal:
Applications of Model Checking at Honeywell Laboratories. 296-303
Electronic Edition (Springer LINK) BibTeX
Bernhard Steffen, Tiziana Margaria, Volker Braun:
Coarse-Granular Model Checking in Practice. 304-312
Electronic Edition (Springer LINK) BibTeX