DIMACS Workshop SPIN96 -- 2nd International SPIN Verification Workshop Algorithms, Applications, Tool Use, Theory: Program

                         Monday, August 5

 8:30- 8:45  === Registration
 8:45- 9:00  === Workshop Opening

 9:00-10:00  Keynote: Automated Verification = Logic + Algorithmics.
                Moshe Vardi (Rice University, USA)

10:00-10:30  Modelling 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 (Verimag/Univ. of Grenoble, France)

10:50-11:20  Proposed Analysis of Synchronous Dual
             Distributed Systems.
                Frank Schneider (NASA/JPL, Fairmont, WV, 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, Bristol, England)
                Ahmed Serhouchni (ENST, Ecole Nationale Superieure
                des Telecommunications, Paris, France)

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, Univ. de Quebec, Canada)
15:50-16:10 Protocol verification with Reactive Promela/RSPIN
                Elie Najm (ENST, Ecole Nationale Superieure
                des Telecommunications, Paris, France),
                Frank Olsen (CNET, Centre National d'Edtudes des
                Telecommunications, Issy-Les-Moulineaux, 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

18:15  Closing, Planning Next Years Workshop

18:30  Workshop Dinner / Hot Buffet

Previous: Participation

Next: Registration

Index

DIMACS Homepage