Date: Saturday, April 5 1997 Place: University of Twente, Enschede, The Netherlands Duration: One day (9am - 5pm)
SPIN is a reachability analysis tool designed for the general verification of distributed systems. First made available publicly in 1991, SPIN is widely used both for teaching and for industrial applications. It has inspired many other tools in various ways.
The first two SPIN workshops, held in Montreal (16 October 1995) and New Jersey (5 August 1996), created opportunities for SPIN users to meet and exchange experiences, ideas, theories, wishes, gripes about formal verification tools.
The SPIN97 workshop will take place following TACAS'97 (Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems), that will take place at the University of Twente on April 2-4 1997. The aim of TACAS'97 is to bring together researchers and practitioners interested in the development and application of tools and algorithms for specification, verification, analysis and construction of distributed and embedded systems. See http://wwwtios.cs.utwente.nl/~tacas97/ for more information.
The SPIN97 workshop will be held at the University of Twente, April 5 1997.
KEYNOTE SPEAKER: Prof. Pierre Wolper (University of Liege)
Rom Langerak (Organization) - langerak@cs.utwente.nl
Gerard J. Holzmann - gerard@research.bell-labs.com
Eli Najm - najm@res.enst.fr
8.30 -- 8.50 Registration
8.50 -- 9.00 Opening
9.00 -- 10.00 Keynote Presentation by
Pierre Wolper (University of Liege):
Where could SPIN go next? A unifying approach
to exploring infinite state spaces.
10.00 -- 10.30 Gerard J. Holzmann (Bell Laboratories):
State Compression in SPIN: Recursive Indexing and
Compression Training Runs.
10.30 -- 11.00 BREAK
11.00 -- 11.30 Hans van der Schoot (University of Ottawa):
Partial-order verification in SPIN can be more efficient.
11.30 -- 12.00 William R. Bevier (Computational Logic, Inc):
Towards an Operational Semantics of PROMELA in ACL2.
12.00 -- 12.30 Carsten Weise (Aachen University of Technology):
An incremental formal semantics for PROMELA
12.30 -- 13.30 LUNCH
13.30 -- 14.00 Siegfried Loeffler, Ahmed Serhouchni (ENST, Paris):
Creating a Validated Implementation of the Steam Boiler
Control.
14.00 -- 14.30 Erich Mikk, Yassine Laknech, Michael Siegel
(Christian-Albrechts University at Kiel):
Towards efficient model checking Statecharts:
A Statecharts to Promela Compiler.
14.30 -- 15.00 Tadashi Nakatani (Toshiba Corporation, Japan):
Verification of Group Address Registration Protocol
using PROMELA and SPIN.
15.00 -- 15.30 BREAK
15.30 -- 16.00 Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi,
Dario Romano, Fernando Torielli, Paolo Traverso (IRST
Trento, ASF Genova, ATR Genova):
Model Checking Safety Critical Software with SPIN:
an Application to a Railway Interlocking System.
16.00 -- 16.30 Peter van Eijk (Utrecht University, EDS):
Verifying Relay Circuits using State Machines.
16.30 -- 17.00 Theo Ruys, Rom Langerak (Twente University):
Validation of Bosch' Mobile Communication Network
Architecture with Spin.
See also the webpage with papers.
* Train. There is a train almost every half hour between Schiphol
International Airport and Enschede. Some services require
you to change trains (at Amersfoort and/or Hengelo).
Once you are in Enschede, you can walk (or catch a taxi)
to the hotel.
* Bus. If you wish to go by bus from Enschede (railway)
station to the university campus, then you need to catch
bus number 1 (the destination is "universiteit").
This service travels every 15 minutes during the day from
the station to the campus.
* Car. The university is well-signposted from all directions.
(It lies half way between Hengelo and Enschede.)
* Taxi. Taxis are available at the train station, of course.
DISH Hotel Boulevard 1945 2 tel: +31 (0)53 486 6666 7511 AE Enschede, The Netherlands fax: +31 (0)53 435 3104The 3-star rooms cost Dfl 100 per night; breakfast (Dfl 17.50) is NOT included in the price. If you want us to make your hotel reservation please register before 21 March (after that date rooms are not guaranteed).
There will be a free shuttle-bus service between the hotel and the university on the day of the workshop. The university is approximately 4 kilometers out of town.
Fill in the form below and send it by e-mail to
langerak@cs.utwente.nl
Remember, if you want us to make a hotel reservation, send this
form before 21 March.
--------------------------------------------------------------------
SPIN97 WORKSHOP AND HOTEL REGISTRATION FORM
University of Twente, The Netherlands, April 5, 1997
--------------------------------------------------------------------
Surname. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Initials . . . . . . . . . . . Title . . . . . . . . . . . . . . . .
Company/Affiliation. . . . . . . . . . . . . . . . . . . . . . . . .
Address. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Postcode . . . . . . City . . . . . . . Country . . . . . . . . . .
Telephone. . . . . . Fax. . . . . . . . E-mail. . . . . . . . . . .
Hotel accommodation (To be paid at the hotel.)
-------------------
Not necessary [ ]
Yes, nights: Fri. 4th Sat. 5th
[ ] [ ]
Dietary restrictions. . . . . . . . . . . . . . . . . . . . . . . . .