--------------------------------------- | The Spin URLs have moved from host | | netlib.bell-labs.com | | to | | netlib.bell-labs.com | ---------------------------------------
Please remember to register. See Newsletter 12 for details on how register by email.
If you register now, registration is free.(And if you register later, it is also free, but you keep us in the dark about the number of lunches to get...)
When: Monday, August 5
Where: Bush Campus, Rutgers University
New Brunswick, New Jersey, USA
8:30- 8:45 === Registration
8:45- 9:00 === Workshop Opening
Keynote
9:00-10:00 Automated Verification = Logic + Algorithmics.
Moshe Vardi (Rice University, USA)
10:00-10:30 Modeling and Analysis of a Collision Avoidance
Protocol using SPIN and UPPAAL.
Henrik Ejersbo Jensen, Kim Larsen,
and Arne Skou (Aalborg University, Denmark)
10:30-10:50 === Coffee Break
Demos:
1. The Wheel environment for SPIN.
F.J. Lin (Bellcore, USA)
2. Real-Time SPIN.
Stavros Tripakis (Univ. of Grenoble, France)
10:50-11:20 Proposed Analysis of Synchronous Dual
Distributed Systems.
Frank Schneider (NASA/JPL, USA)
11:20-11:50 Memory efficient storage in SPIN.
Willem Visser (Univ. of Manchester, England)
11:50-12:20 Dynamic analysis of SA/RT Models Using SPIN.
Javier Tuya, Jose de Diego, Claudio de la Riva,
and Jose Corrales, (Univ. de Oviedo, Spain)
12:20-13:30 === Lunch
13:30-14:00 The Application of Promela and SPIN in
the BOS Project.
Pim Kars (Twente Univ., The Netherlands)
14:00-14:30 Modeling and verification of the ITU-T multipoint
communication service with SPIN.
P. Merino, J.M. Troya (Univ. de Malaga, Spain)
14:30-14:50 Creating Implementations from Promela Models.
Siegfried Loeffler (Hewlett-Packard, England)
Ahmed Serhouchni (ENST, Paris)
14:50-15:10 === Coffee Break
Demo by Siegfried Loeffler (Promela2C translator)
15:10-15:30 On Nested Depth-First Search
Gerard Holzmann, Doron Peled,
Mihalis Yannakakis (Bell Labs, USA)
15:30-15:50 State space compression in SPIN with GETSs
Jean-Charles Gregoire (INRS, Canada)
15:50-16:10 Protocol verification with Reactive Promela/RSPIN
Elie Najm (ENST, France),
Frank Olsen (CNET, France)
16:10-16:30 === Coffee Break
Demo by Frank Olsen (RSPIN)
16:30-16:50 Implementing and Verifying Scenario-Based
specifications using Promela/SPIN.
Stefan Leue (Univ. Waterloo, Canada)
Peter Ladkin (Univ. Bielefeld, Germany)
16:50-17:10 Simulation and Validation Tool for self-stabilizing
protocols.
Sandeep Shukla, Daniel J. Rosenkrantz,
S.S. Ravi (Univ. at Albany, NY, USA)
17:10-17:30 Not checking for closure under stuttering
Gerard Holzmann (Bell Labs, USA)
Orna Kupferman (Berkely Univ., USA)
17:30-17:45 === Short Break
17:45-18:15 === Panel Session (tba)
18:15 Closing, Planning Next Years Workshop
18:30 Workshop Dinner / Hot Buffet
Gerard J. Holzmann (gerard@research.bell-labs.com)