SPIN NEWSLETTER Nr. 13

SPIN NEWS - Nr. 13 - July 5, 1996

Contents of this NewsLetter:

Change of URLs

---------------------------------------
| The Spin URLs have moved from host   |
|        netlib.bell-labs.com                 |
| to                                    |
|        netlib.bell-labs.com           |
---------------------------------------

SPIN96 Workshop News

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...)

PRELIMINARY WORKSHOP PROGRAM:

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

End of Newsletter Nr. 13.

Gerard J. Holzmann (gerard@research.bell-labs.com)