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 gregoire@inrs-telecom.uquebec.ca.

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

erdogmus@iit.nrc.ca

Checking Linear Temporal Logic Properties

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

doron@research.bell-labs.com, gerard@research.bell-labs.com

Partial Order Reduction of the State Space

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

doron@research.bell-labs.com, gerard@research.bell-labs.com

The ULG Partial Order Package for SPIN

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

god@research.bell-labs.com

Issues in State Space Reduction

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

gregoire@inrs-telecom.uquebec.ca

Security Protocol Verification using SPIN

Audun Joesang, Norwegian Inst. of Technology, Norway

ajos@idt.unit.no

Implementing MSCs in PROMELA

Stefan Leue, University of Waterloo, Canada

sleue@swen.UWaterloo.ca

Reactive SPIN and PROMELA

Elie Najm and Fred Olsen, ENST, France

najm@res.enst.fr

Industrial experience with formal validation

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

markstas@research.bell-labs.com

Process Control Design Using SPIN

Thierry Cattel, EPFL, Switzerland

cattel@di.epfl.ch

Modeling and Verification of the RUBIS micro-kernel with SPIN

Greg Duval and Jacques Julliand, EPFL, Switzerland

Gregory.Duval@di.epfl.ch

Design of a Storm Surge Barrier control System

Pim Kars, Univ. Twente, The Netherland

kars@cs.utwente.nl

Two applications of PROMELA/SPIN

F. Joe Lin, Bellcore, NJ, USA

fjlin@bellcore.com

SPIN as a Hardware Design Tool

Budi Rahardjo, U. of Manitoba, Canada

rahard@ee.umanitoba.ca

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

manione@scsun4.CSELT.STET.IT

Extending PROMELA and SPIN for Real-Time

Stavros Tripakis and Costas Courcoubetis, Crete

tripaki@csd.uch.gr, courcou@ics.forth.gr

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