SPIN99 Workshop V - Online Proceedings
SPIN99 - Papers
from the 5th International
SPIN Workshop
The 5th SPIN workshop was held on Monday July 5, 1998,
at the start of the Federated Logic 1999 Conference in
Trento, Italy.
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.
John Rushby
Computer Science Laboratory,
SRI International, Menlo Park, California, USA.
Abstract:
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.
Runtime efficient state compaction in Spin.
J. Geldenhuys and P.J.A. de Villiers,
{jaco,pja}@cs.sun.ac.za,
Dept. of Computer Science, Univ. of Stellenbosch,
South Africa.
Postscript: compaction.ps.gz (12 pgs.)
Distributed-Memory model checking with Spin.
F. Lerda, and R. Sisto,
flerda@athena.polito.it, sisto@polito.it,
Politecnico di Torino, Italy.
Postscript: distributed.ps.gz (15 pgs.)
Partial order reduction in presence of rendez-vous communications
with unless constructs and weak fairness.
D. Bosnacki,
dragan@win.tue.nl,
Eindhoven University, The Netherlands.
Postscript: dragan.ps.gz (17 pgs.)
Adding active objects to Spin.
W. Visser, K. Havelund, and J. Penix,
wvisser@ptolemy.arc.nasa.gov,
RIACS, Recom, NASA Ames, USA,
Postscript: visser.ps.gz (11 pgs.)
Model checking of Manifold applications with the Spin model checker.
A. Fagot, and A. Scutella,
{adriano, fagot}@cwi.nl,
CWI, Amsterdam, The Netherlands,
Postscript: manifold.ps.gz (20 pgs.)
Divide, abstract, and model-check.
K. Stahl, K. Baukus, Y. Lakhnech, M. Steffen,
{kst,kba,ms}@informatik.uni-kiel.de
Univ. of Kiel, Germany,
Postscript: divide.ps.gz (20 pgs.)
Workshop Organization
Dennis Dams (Eindhoven University): D.R.Dams@ele.tue.nl
Mieke Massink (CNR-Ist. CNUCE, Pisa): m.massink@guest.cnuce.cnr.it
Ed Brinksma (Univ. of Twente)
Marco Daniele (ITC-IRST, Trento)
Bengt Jonsson (Uppsala University)
Gerard Holzmann (Bell Labs)
Online Proceedings for Previous Spin Workshops
- Spin95,
Oct. 1995, Montreal, Canada
- Spin96,
Aug. 1996, Rutgers University, USA
- Spin97,
April 1997, Twente University, The Netherlands
- Spin98,
November 1998, ENST, Paris, France
Spin homepage:
http://netlib.bell-labs.com/netlib/spin/whatispin.html