Abstracts from SPIN95, the First SPIN Workshop

Held at INRS-Télécommunications, Montréal, Quebec

On 16 October 1995

Index of Papers Presented at the Workshop:

  1. Verifying Semantic Relations in SPIN
  2. Checking Linear Temporal Logic Properties
  3. Partial Order Reduction of the State Space
  4. The ULG Partial Order Package for SPIN
  5. Issues in State Space Reduction
  6. Security Protocol Verification using SPIN
  7. Implementing MSCs in PROMELA
  8. Reactive SPIN and PROMELA
  9. Industrial experience with formal validation
  10. Process Control Design Using SPIN
  11. Modeling and Verification of the RUBIS micro-kernel with SPIN
  12. Design of a Storm Surge Barrier control System
  13. Two applications of PROMELA/SPIN
  14. SPIN as a Hardware Design Tool

Index of Complementary Material:

  1. Interactive Timed Simulation of Distributed Systems
  2. Extending PROMELA and SPIN for Real-Time
  3. Specification and Verification of the Implementation Behavior of a Wireless LAN Controller Chip using PROMELA and SPIN
  4. Using OBDD Encodings for Space Efficient State Storage during On-the-fly Model Checking

Participation

29 people participated in the workshop, 13 from Canada, 8 from the USA, and 8 from Europe (France, Norwary, Switzerland, and The Netherlands). 14 research papers were presented at the workshop; 4 other contributions arrived too late to be included, or could not be presented at the workshop itself but are included as complementary material here.

Printed Proceedings

A small number of printed proceedings from the workshop may still be available. If you are interested in obtaining a copy, please contact the SPIN95 workshop organizer Jean-Charles Grégoire at [email protected]

SPIN96?

The SPIN workshop created a wonderful opportunity for SPIN users, and many others seriously interested in verification tools and on-the-fly model checking techniques, to meet and interact directly to exchange experiences, ideas, theories, wishes. The overal quality of the contributions was outstanding and inspiring. We will therefore go ahead with our tentative plan to prepare for a Second Workshop (SPIN96) in New Jersey in 1996, most likely adjacent to the CAV96 conference (which is held from 31 July to August 3 1996 at Rutgers University in New Brunswick, New Jersey). Details about precise dates, location, and submission deadlines will follow in the next few months. The most likely victims to organize SPIN96 are Doron Peled, Gerard Holzmann, and Jean-Charles Grégoire.

Abstracts:

Verifying Semantic Relations in SPIN

Hakan Erdogmus, National Research Council, Canada

[email protected]

Checking Linear Temporal Logic Properties

Doron Peled and Gerard Holzmann, AT&T Bell Laboratories, NJ, USA

[email protected], [email protected]

Partial Order Reduction of the State Space

Doron Peled and Gerard Holzmann, AT&T Bell Laboratories, NJ, USA

[email protected], [email protected]

The ULG Partial Order Package for SPIN

Patrice Godefroid, AT&T Bell Laboratories, IH, USA

[email protected]

Issues in State Space Reduction

Jean-Charles Grégoire, INRS-Télécom, Canada

[email protected]

Security Protocol Verification using SPIN

Audun Joesang, Norwegian Inst. of Technology, Norway

[email protected]

Implementing MSCs in PROMELA

Stefan Leue, University of Waterloo, Canada

[email protected]

Reactive SPIN and PROMELA

Elie Najm and Fred Olsen, ENST, France

[email protected]

Industrial experience with formal validation

Mark Staskauskas, AT&T Bell Labs, IH, USA

[email protected]

Process Control Design Using SPIN

Thierry Cattel, EPFL, Switzerland

[email protected]

Modeling and Verification of the RUBIS micro-kernel with SPIN

Greg Duval and Jacques Julliand, EPFL, Switzerland

[email protected]

Design of a Storm Surge Barrier control System

Pim Kars, Univ. Twente, The Netherland

[email protected]

Two applications of PROMELA/SPIN

F. Joe Lin, Bellcore, NJ, USA

[email protected]

SPIN as a Hardware Design Tool

Budi Rahardjo, U. of Manitoba, Canada

[email protected]

Other Papers

(Submitted but not presented at the workshop itself)

Interactive Timed Simulation of Distributed Systems --- from PROMELA to PROMELA+

Marco Daniele, Paola Renditore, and Roberto Manione, CSELT, Italy

[email protected]

Extending PROMELA and SPIN for Real-Time

Stavros Tripakis and Costas Courcoubetis, Crete

[email protected], [email protected]

Specification and Verification of the Implementation Behavior of a Wireless LAN Controller Chip using PROMELA and SPIN

Michael Griffioen, AT&T Network Wireless Systems, The Netherlands

Using OBDD Encodings for Space Efficient State Storage during On-the-fly Model Checking

Willem C. Visser, Manchester Univ., UK

Return to

Index of Spin Newsletters