Formal Methods for Industrial Critical Systems
FMICS 2001
Paris, 16-17 July 2001
| 6th
International Workshop on
Formal Methods for Industrial Critical Systems FMICS 2001 Paris, 16-17 July 2001 |
|
| 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
|
