SPIN99 Workshop V - Online Proceedings
SPIN99 - Papers
from the 5th International
The 5th SPIN workshop was held on Monday July 5, 1998,
at the start of the Federated Logic 1999 Conference in
Below is the list of papers presented at the workshop,
in order of presentation, with links to the postscript
for online versions where available.
Keynote: Integrated Formal Verification:
Using Model Checking with Automated Abstraction,
Invariant Generation, and Theorem Proving.
Runtime efficient state compaction in Spin.
Computer Science Laboratory,
SRI International, Menlo Park, California, USA.
Modern formal verification tools are quite effective,
but they might become even more effective if used in
combination and supported by ancillary tools.
For example, automated abstractions could ease construction
of the finite-state models needed for model checking, and
a combination of theorem proving and model checking could
extend the reach of highly automated verification.
There are at least a couple of projects (SAL at SRI and
Stanford, and Veritech at The Technion) that are building
experimental systems to support these integrated approaches.
I will describe the general architecture of these systems,
the methodologies envisaged for their use, a few of the
techniques developed to perform the ancillary tasks, and
some of the results obtained so far. I will also outline
how existing tools such as model checkers and theorem
provers can best contribute to, and take advantage of
these integrated frameworks.
J. Geldenhuys and P.J.A. de Villiers,
Dept. of Computer Science, Univ. of Stellenbosch,
Postscript: compaction.pdf (12 pgs.)
Distributed-Memory model checking with Spin.
F. Lerda, and R. Sisto,
Politecnico di Torino, Italy.
Postscript: distributed.pdf (15 pgs.)
Partial order reduction in presence of rendez-vous communications
with unless constructs and weak fairness.
Eindhoven University, The Netherlands.
Postscript: dragan.pdf (17 pgs.)
Adding active objects to Spin.
W. Visser, K. Havelund, and J. Penix,
RIACS, Recom, NASA Ames, USA,
Postscript: visser.pdf (11 pgs.)
Model checking of Manifold applications with the Spin model checker.
A. Fagot, and A. Scutella,
CWI, Amsterdam, The Netherlands,
Postscript: manifold.pdf (20 pgs.)
Divide, abstract, and model-check.
K. Stahl, K. Baukus, Y. Lakhnech, M. Steffen,
Univ. of Kiel, Germany,
Postscript: divide.pdf (20 pgs.)
Mieke Massink (CNR-Ist. CNUCE, Pisa)
Ed Brinksma (Univ. of Twente)
Marco Daniele (ITC-IRST, Trento)
Bengt Jonsson (Uppsala University)
Gerard Holzmann (Bell Labs)
Online Proceedings for Previous Spin Workshops
Oct. 1995, Montreal, Canada
Aug. 1996, Rutgers University, USA
April 1997, Twente University, The Netherlands
November 1998, ENST, Paris, France