6th International Workshop on
Formal Methods for Industrial Critical Systems
FMICS 2001
Paris, 16-17 July 2001

Workshop Programme

16 July 2001
8.00 - 9.00 Registration
9.00 - 9.10 Welcome by Jean-Eric Pin (Scientific Director of ERCIM France)
9.10 - 10.10 Invited Presentation: Cindy Eisner (IBM Research, Haifa).
Automatic Detection of Vacuity in Temporal Logic.
10.10 -10.40 Coffee Break
10.40 - 11.15 JF Groote (Eindhoven Uni), J Pang (CWI Amsterdam), AG Wouters (CWI Amsterdam).
A Balancing Act: Analyzing a Distributed Lift System.
11.15-11.50 A Kervinen (Tampere Uni), A Valmari (Tampere Uni), R Jarnstrom (Instrumentointi Oy, Tampere).
Debugging a Real-Life Protocol with CFFD-Based Verification Tools.
11.50 - 12.25 A Pretschner (TU Munich), O Slotosch (Validas, Munich), H Lötzbeyer (TU Munich), E Aiglstorfer (Giesecke & Devrient, Munich), 
S Kriebel (Giesecke & Devrient, Munich). Model-Based Testing for Real: The Inhouse Card Case.
12.25 - 14.00 Lunch
14.00 - 14.35 L Mikhailov (Southampton Uni), M Butler (Southampton Uni).
Combining B and Alloy.
14.35 - 15.10 T Zheng (Concordia Uni Montreal), F Khendek (Concordia Uni Montreal).
Service Specification and Analysis using Message Sequence Charts.
15.10 - 15.45 T Arts (Ericsson, Älvsjö), CB Earle (Ericsson, Älvsjö).
Development of Verified Erlang Programs.
15.45 - 16.15 Coffee Break
16.15 - 16.50 D Beyer (TU Cottbus), A Noack (TU Cottbus).
Verification of Timed Automata using BDDs.
16.50 - 17.25 V Charchiolo (Catania Uni), N De Francesco (Pisa Uni), A Fantechi (Florence Uni), G Mangioni (Catania Uni).
ESA: An APproach to Systems Design by Equation Solving.
17.25 - 18.00 J Power (Maynooth Uni), D Sinclair (Dublin City Uni).
A Formal Model of Forth Control Words in the Pi-Calculus.
20.00 - 23.00 Workshop Dinner (on the Eiffel Tower)
17 July 2001
9.00 - 10.00 Invited Presentation: Joseph Sifakis (Vérimag, Grenoble).
Modeling Real-time Systems.
10:00 - 10.30 Coffee Break
10.30 - 11.05 D Bustan (Technion, Haifa), O Grumberg (Technion, Haifa).
Modular Minimization of Deterministic Finite-State Machines.
11.05 - 11.40 G Pace (Vérimag, Grenoble), N Halbwachs (Vérimag, Grenoble), P Raymond (Vérimag, Grenoble).
Counter-Example Generation in Symbolic Abstract Model-Checking.
11.40 - 12.15 M Maidl (Edinburgh Uni).
Localizing Model-Checking by Analyzing Transitions.
12.15 - 14.00 Lunch
14.00 - 14.35 M Majster-Cederbaum (Mannheim Uni), F Salger (Mannheim Uni).
Towards the Efficient Development of Correct Reactive Systems.
14.35 - 15.10 M Bozga (Vérimag, Grenoble), L Mounier (Vérimag, Grenoble), D Lesens (EADS Launch Vehicles).
Model-Checking Ariane-5 Flight Program.
15.10 - 15.45 C Montangero (Pisa Uni), L Semini (Pisa Uni).
Software Specification and Design: From Formal Methods to Standard Middleware.
15.45 Closing of Workshop
16.00 - 17.00 FMICS Working Group Meeting

(c) 2000 Ulrich Ultes-Nitsche