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,
erdogmus@iit.nrc.ca
Verifying Semantic Relations in SPIN*
-
10:30-11:00 Doron Peled, AT&T Bell Laboratories,
doron@research.bell-labs.com
Checking Linear Temporal Logic Properties
& Partial Order Reduction of the State Space
-
11:00-11:30 Patrice Godefroid, AT&T Bell Laboratories,
god@graceland.ih.att.com
The ULG Partial Order Package for SPIN
-
11:30-12:00 J-Ch. Gregoire, INRS-Telecom,
gregoire@inrs-telecom.uquebec.ca
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,
ajos@idt.unit.no
Security Protocol Verification using SPIN
-
13:30-14:00 Stefan Leue, University of Waterloo,
sleue@swen.UWaterloo.ca
Implementing MSCs in PROMELA
-
14:00-14:30 Elie Najm, ENST,
najm@res.enst.fr
Reactive SPIN and PROMELA
-
14:30-15:00 Mark G. Staskauskas, AT&T Bell Laboratories,
markstas@research.att.com
Industrial Experience with Formal Validation
Late afternoon session: 15:15 -> 17:15
-
15:15-15:45 Thierry Cattel and Greg Duval, EPFL,
cattel@di.epfl.ch
Process Control Design Using SPIN
-
15:45-16:15 Pim Kars, Univ. Twente,
kars@cs.utwente.nl
Design of a Storm Surge Barrier control System
-
16:15-16:45 F. Joe Lin, Bellcore,
fjlin@bellcore.com
Two applications of PROMELA/SPIN
-
16:45-17:15 Budi Rahardjo, U. of Manitoba,
rahard@ee.umanitoba.ca
SPIN as a Hardware Design Tool
Wrapup and Closing
End of Newsletter Nr. 8
Gerard J. Holzmann
(gerard@research.bell-labs.com)