FMICS 2009 - PROGRAM
Please visit: http://users.dsic.upv.es/workshops/fmics2009


************************************************************
*             14th International Workshop on               *
*      Formal Methods for Industrial Critical Systems      *
*                      FMICS 2009                          *
*                                                          *
*                   November 2-3, 2009                     *
*               Eindhoven, The Netherlands                 *
************************************************************



Monday 2 November
*****************

9h-9h05 FMICS 2009 Opening (Maria Alpuente)

9h05-10h Invited Talk (Chair: Maria Alpuente) 

Ken McMillan 
Cadence, USA
What's in Common Between  Test, Model Checking, and Decision
Procedures?

**********************
10h-10h30 Coffee Break
**********************

10h30-11h30 Session 1 (Chair: Jaco van de Pol)

David  Delmas, Eric  Goubault, Sylvie  Putot, Jean  Souyris,
Karim Tekkal and Franck Vedrine.
Towards  an Industrial  Use of  FLUCTUAT on  Safety-Critical
Avionics Software

Alwyn Goodloe and Cesar Munoz. 
Compositional Verification of a Communication Protocol for a
Remotely Operated Vehicle

11h30-12h Poster Session 1 (Chair: Ken McMillan)

Alessio Ferrari, Alessandro  Fantechi, Stefano Bacherini and
Niccolo Zingoni.
Formal  Development for  Railway Signaling  Using Commercial
Tools

Nassima Izerrouken, Marc Pantel, Xavier Thirioux and Olivier
Ssi Yan Kai.
Integrated Formal  Approach for Qualified  Critical Embedded
Code Generator

Laura  Panizo,  Maria del  Mar  Gallardo,  Pedro Merino  and
Antonio Linares.
Developing a  Decision Support Tool for  Dam Management with
SPIN

*****************
12h30-14h30 Lunch 
*****************

14h30-15h30 Invited Talk (Chair: Stefania Gnesi) 

Dino Distefano
Queen Mary, University of London, UK
Attacking Large Industrial Code with Bi-Abductive Inference

**********************
15h30-16h Coffee Break
**********************

16h-17h30 Session 2 (Chair: Dino Distefano)

Jose Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto and
Bárbara Vieira.
Correctness with Respect to Reference Implementations

Erik Schierboom, Alejandro Tamalet,  Hendrik Tews, Marko van
Eekelen and Sjaak Smetsers.
Preemption Abstraction: a  Lightweight Approach to Modelling
Concurrency.

Javier de Dios and Ricardo Pena. 
A  Certified  Implementation  on  top of  the  Java  Virtual
Machine

*************************************
19h30 Workshop Dinner and EASST award
*************************************

Tuesday 3 November
******************

9h-10h Invited Talk (Chair: Alessandro Fantechi) 

Diego Latella
ISTI/CNR, Italy
On  a Uniform  Framework  for the  Definition of  Stochastic
Process Languages

**********************
10h-10h30 Coffee Break
**********************

10h30-12h Session 3 (Chair: Santiago Escobar)

Matthias  Raffelsieper,   MohammadReza  Mousavi,  Jan-Willem
Roorda, Chris Strolenberg and Hans Zantema.
Formal Analysis  of Non-Determinism in Verilog  Cell Library
Simulation Models

Julio Marino,  Angel Herranz, Manuel Carro  and Juan Jose
Moreno-Navarro.
Formal Modeling of Concurrent Systems with Shared Resource

Kenneth J. Turner and Koon Leai Larry Tan. 
A Rigorous Methodology for Composing Services

*****************
12h-14h Lunch 
*****************

14h-15h Invited Talk (Chair: Diego Latella) 

Thierry Lecomte
ClearSy, France
Applying a Formal Method in Industry: a 15-year trajectory

15h-15h30 Poster Session 2 (Chair: Maria del Mar Gallardo)

Lukas Ladenberger, Jens Bendisposto and Michael Leuschel.
Visualizing Event-B models with BMotionStudio 

Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans
and Ronny Wichers Schreur.
Model-Based Testing of Electronic Passports

Aad Mathijssen, Yaroslav S. Usenko and Dragan Bosnacki. 
Behavioural Analysis of an I2C Linux Driver 

**********************
15h30-16h Coffee Break
**********************

16h-17h Session 4 (Chair: Christophe Joubert)

Pavel Parizek and Tomas Kalibera. 
Platform-Specific  Restrictions  on   Concurrency  in  Model
Checking of Java Programs

Sami Evangelista and Lars Michael Kristensen. 
Dynamic State  Space Partitioning for External  Memory Model
Checking

17h30-18h30 FMICS 2009 Closure and FMICS Working Group Meeting