Specification and Validation
of Reactive Systems

Workshop organized by
the Vires LTR-project.

June 14th-15th

At Autrans (Escandille)

VIRES (Verifying Industrial REactive Systems) is an LTR-ESPRIT project carried out by an international consortium comprising of the Universities of Grenoble (Verimag), Liege and Kiel and led by the Eindhoven University of Technology.
The objective of the project is to develop a family of interconnected tools for the analysis of protocols of industrial size and to advance the state of the art in modeling and analyzing reactive systems.

The consortium of VIRES organizes a workshop on the

Specification and Validation of Reactive Systems.

The workshop will present the state of the art in the field of specification and validation of reactive systems.

Venue: The workshop will take place at Autrans a village at 1050 m located at the heart of the Vercors massif in a landscape of pastures and forests.

Talks:

On-the-fly test synthesis with TGV. Thierry Jeron , Irisa/INRIA, Rennes, France. Abstract.Slides.
Games and abstract games in the verification of protocols.Perdita Stevens, Division of Informatics, University of Edinburgh. Abstract.
Bandera : Extracting Finite-state Models from Java Source Code.Matthew Dwyer, Kansas State University, USA. Abstract.
Proving Properties of C programs. Gerard J. Holzmann, Computing Principles Research, Bell Labs, USA. Abstract.
Beyond Program Analysis: Profiles and Heterogeneity. B. Steffen, University of Dortmund. Abstract. Slides.
Uniform Verification of Parameterized Networks. Amir Pnueli, Weizmann Institute, Israel. Abstract. Slides.
The application of formal techniques within the software life cycle of safety critical applications. Paolo Traverso, Automated Reasoning Systems Division at IRST, Trento (Italie). Abstract.
LPV: a new technique to formally prove or disprove safety properties. Jean-Luc Lambert (Valiosys). Abstract.
A Methodology for the Construction of Scheduled Systems. Joseph Sifakis, Verimag.
A Practical Approach to Verifying Infinite State Systems. P. Wolper, University of Liege.
Model Checking a Medium Access Control Protocol. D. Dams ,TU Eindhoven. Abstract. Slides
Stochastic Process Algebras: Linking Process Descriptions with Performance. Ed Brinksma. University of Twente. Abstract.Slides.

Tentative Schedule: June 14th

9:25- 9:30	Welcome
9:30- 10:30	Proving Properties of C programs. G. J. Holzmann.
10:30 - 11:00	Coffee Break
11:00- 12:00	A Practical Approach to Verifying Infinite State Systems. P. Wolper.
12:00 - 13:30	Lunch
13:30 - 14:30	Games and abstract games in the verification of protocols. P. Stevens.
14:30-15:30	The application of formal techniques within the software life cycle of safety critical applications. Paolo Traverso.
15:30- 16:00	Coffee Break
16:00- 17:00	On-the-fly test synthesis with TGV. T. Jeron.
17:00 - 18:00	Stochastic Process Algebras: Linking Process Descriptions with Performance. Ed Brinksma.

June 15th

8:30 -9:30	Uniform Verification of Parameterized Networks. A. Pnueli.
9:30 - 10:00	Coffee Break
10:00 - 11:00	Beyond Program Analysis: Profiles and Heterogeneity. B. Steffen
11:00 - 11:15	Break
11:15 - 12:15	Bandera : Extracting Finite-state Models from Java Source Code. M. Dwyer
12:15 - 14:00	Lunch
14:00 - 15:00	LPV: a new technique to formally prove or disprove safety properties. J.-L. Lambert
15:00- 15:30	Coffee Break
15:30 - 16:30	A Methodology for the Construction of Scheduled Systems. J. Sifakis.
16:30 - 16:45	Break
16:45 - 17:45	Model Checking a Medium Access Control Protocol. D. Dams

Registration: To register fill this form and send it by fax and by mail to the following address:

     Jeanne-Marie Colle,
       Verimag
       Centre Equation, 2 av. de Vignate, 38610 Gieres, France.
       Fax: (33-476) 6348-18
       Tel.: (33-476) 6348-57
        email: jmcolle@imag.fr

Travel Information:
A bus (named PHILIBERT)from Grenoble to Autrans on June 14th will be organized. It will departure at 8h30 from the airport bus station which is close to the train station.
Public transportation .
See also information at access.
Hotel in Grenoble:
We reserved rooms in the Hotel Touring, 26 Avenue Alsace Loraine , Tel: (33-4)76462432, fax: (33-4)76460285. Contact the hotel to book a room.