Specification and Validation
of Reactive Systems
Workshop organized by
the Vires LTR-project.
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
The workshop will present the state of the art in the field of specification and validation of reactive systems.
workshop will take place at
village at 1050 m located at the heart of the Vercors
massif in a landscape of pastures and forests.
|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.|
|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|
register fill this form and send
it by fax and by mail to the following address: