SPIN NEWS - Nr. 8 - October 12, 1995

Final Details on the SPIN Workshop

Date: Monday October 16, 1995

Participation:

We have a very good level of participation in the first SPIN Workshop. So far, approximately 25 people have registered, and about half of the participants have promised to present some of their work. It promises to be an interesting day. The papers presented will be collected in a workshop proceedings that is available to all participants. Late registrants are of course always welcome on the 16th.

Location:

INRS-Telecommunications, 16, Place du Commerce, Nuns' Island, Montreal

INRS-Telecommunications is located in the premises of BNR-Montreal. We'll assemble in the lobby of INRS around 9:45am, and we'll be escorted to the conference room.

Transportation from downtown Montreal:

By Bus:
Take bus 168 from the corner of Union and Ste Catherine, to the 2nd stop on the island, after the bus leaves the highway (about a 15 minute ride).

By Taxi
From downtown Montreal the ride costs about CN$ 10. For those staying in the FORTE conference hotel, well meet at 9:30 am in the hotel lobby and share taxis to INRS.

Workshop Agenda:

Morning session: 10:00 -> 12:30

10:00-10:30 Hakan Erdogmus, National Research Council, [email protected]
Verifying Semantic Relations in SPIN*
10:30-11:00 Doron Peled, AT&T Bell Laboratories, [email protected]
Checking Linear Temporal Logic Properties & Partial Order Reduction of the State Space
11:00-11:30 Patrice Godefroid, AT&T Bell Laboratories, [email protected]
The ULG Partial Order Package for SPIN
11:30-12:00 J-Ch. Gregoire, INRS-Telecom, [email protected]
Issues in State Space Reduction

Open Discussion 12:00-12:15

Lunch on location: 12:15-13:00

Early afternoon session 13:00 -> 15:00

13:00-13:30 Audun Joesang, Norwegian Inst. of Technology, [email protected]
Security Protocol Verification using SPIN
13:30-14:00 Stefan Leue, University of Waterloo, [email protected]
Implementing MSCs in PROMELA
14:00-14:30 Elie Najm, ENST, [email protected]
Reactive SPIN and PROMELA
14:30-15:00 Mark G. Staskauskas, AT&T Bell Laboratories, [email protected]
Industrial Experience with Formal Validation

Late afternoon session: 15:15 -> 17:15

15:15-15:45 Thierry Cattel and Greg Duval, EPFL, [email protected]
Process Control Design Using SPIN
15:45-16:15 Pim Kars, Univ. Twente, [email protected]
Design of a Storm Surge Barrier control System
16:15-16:45 F. Joe Lin, Bellcore, [email protected]
Two applications of PROMELA/SPIN
16:45-17:15 Budi Rahardjo, U. of Manitoba, [email protected]
SPIN as a Hardware Design Tool