Dear all,

Sorry for the multiple posts



ISoLA Workshop On Leveraging Applications of 
Formal Methods, Verification and Validation
Special Workshop Theme: Formal Methods in Avionics, Space and Transport
ENSMA - Poitiers December 12-14
Information about participation available on

Scientific Programme

Wednesday December 12
11h  12h Registration
12h Lunch
13h45  14h Welcome
14h  15h Invited talk Avionic Software 
Verification by Abstract Interpretation.
By Patrick COUSOT. LIENS - Ecole Normale Supérieure de Paris- Paris, France.
15h  15h30 Break
15h30  17h30 Session 1. Scheduling
  “New worst-case analysis technique for real-time transactions”
By AhmedRahni, Emmanuel Grolleau and Michaël 
Richard - LISI/ENSMA, Futuroscope, France.
“A C-space sensitivity analysis of Earliest Deadline First scheduling”
By Jean-François Hermant - ECE, LACSC, Paris, 
France - and Laurent George - University of Paris 12, France.
“Functionally Deterministic Scheduling”
By Frédéric Boniol - IRIT-ENSEEIHT, Toulouse, 
France -, Claire Pagetti, and François Revest - ONERA-CERT, Toulouse, France.
“Reliable and Precise WCET and Stack Size 
Determination for a Real-life Embedded Application”
By PhilippeBaufreton - Hispano-Suiza, 
Etablissement de Réau, Moissy-Cramayel, France - 
and Reinhold Heckmann  AbsInt Angewandte 
Informatik GmbH, Saarbrücken, Germany.

17h30 Social event

Thursday December 13
8h30  9h30 Invited talk. “Model-based development 
of embedded control systems: historical perspective and recent advances”
By Paul CASPI. Former researcher Verimag-Grenoble, France.
9h30  10h30 Session 2. Performance Analysis
“Formal models of Fractal Component Based Systems for performance analysis”
By Nabila Salmi, Patrice Moreaux - Université de 
Savoie, France -, and Malika Ioualalen - USTHB, Algiers, Algeria.
“Fault-Tolerance Analysis of Mixed CAN/Switched Ethernet Architecture”
By Claudia Betous-Almeida, Jean-Luc Scharbarg, 
and Christian Fraboul - IRIT-ENSEEIHT- University of Toulouse, France.

10h30  11h BREAK
11h  12h30 Session 3. Model Checking
“Seven at one stroke: LTL model checking for 
High-level Specifications in B, Z, CSP, and more”
By Michael Leuschel and Daniel Plagge - Institut 
für Informatik, Heinrich-Heine-Universität Düsseldorf, Germany.
“Verification, Diagnosis and Adaptation: Tool 
supported enhancement of the model-driven verification process”
By Marco Bakera, Tiziana Margaria, Clemens D. 
Renner - University of Potsdam, Germany -, and 
Bernhard Steffen - University of Dortmund, Germany.
“Verification of embbeded systems with preemption: a negative result”
By Jérôme Ermont and Frédéric Boniol - 
IRIT-ENSEEIHT - University of Toulouse, France.

12h30  14h Lunch

14h  15h Invited talk “The aeronautical systems 
development challenges for Airbus”
By Odile LAURENT. Airbus France  Toulouse, France.
15h  16h Session 4. Formal Modelling
“Using Analogy to Promote Conceptual Modeling Reuse”
By Karin K. Breitman, Simone D.J. Barbosa, Marco 
A. Casanova, Antonio L. Furtado - Pontifícia 
Universidade Católica do Rio de Janeiro, Brazil 
-, Michael G. Hinchey - Loyola College, Baltimore, USA.
“Formal Modeling of Data. A Case Study for Space Applications”
By Jean-Paul BLANQUART  Astrium Satellites, 
Toulouse, France - GérardBulsa  ESTEC Keperlaan, 
Noordwijk, Netherlands -, David Lesens  Astrium 
Space Transportation, Les mureaux, France -, 
George Mamais  Semantix Information Technologies, 
Athens, Greece -  and Maxime Perrotin  ESTEC Keperlaan, Noordwijk, Netherlands.

16h  16h30 Break
16h30  18h Session 5. Refinement / Abstraction Methods
“Don't care in SMT-Building flexible yet 
efficient abstraction/refinement solvers”
By Andreas Bauer - Canberra Research Laboratory, 
Australia - , Martin Leucker, Christian 
Schallhart, and Michael Tautschnig - Technische Universität München, Germany.
“Qualitative Abstraction based Verification for Analog Circuits”
By Mohamed H. Zaki, Sofiène Tahar - Concordia 
University, Montréal Canada - and Guy Bois - 
Ecole Polytechnique de Montreal, Canada.
“Preservation of timed properties during an 
incremental development by components”
By Jacques Julliand, Hassan Mountassir, and 
Emilie Oudot - Université de Franche-Comté, France.

19h30 Social event

Friday December 14
8h30  9h30 Invited talk “Development of Transportation Systems”
By Dines BJORNER. Technical University of Denmark - Lingby, Denmark.
9h30  10h30 Session 6. Real Time
“OASIS formal approach for distributed 
safety-critical real-time system design”
By Jean-Sylvain Camier, Damien Chabrol, Vincent 
David, and Christophe Aussaguès  CEA, GIF SUR YVETTE, France.
“Proved Development of the Real-Time Properties 
of the IEEE 1394 Root Contention Protocol with the Event B Method”
By Joris Rehm - Université Henri Poincaré Nancy 
1, France - and DominiqueCansell  LORIA, France.

10h30  11h Break
11h  12h30 Session 7. Testing
“A Simplified Approach for Testing Real-Time 
Systems Based on Action Refinement”
By Saddek Bensalem, Moez Krichen - Verimag 
Laboratory, Gières, France -, Lotfi Majdoub, 
Riadh Robbana - LIP2 Laboratory and Polytechnic 
School of Tunisia, Tunisia - and Stavros Tripakis 
- Verimag Laboratory and Cadence Berkeley Labs, USA.
“Using Formal Methods to increase confidence in 
one Home Network System implementation. Case study”
By Lydie du Bousquet - Universités de Grenoble, 
France -, MasahideNakamura - Kobe University, 
Japan -, Ben Yan - Nara Institute of Science and 
Technology, Japan -  and Hiroshi Igaki - Kobe University, Japan.
“Using Invariant Detection Mechanism in Black Box Inference”
By Muzammil Shahbaz - France Telecom R&D, Meylan, 
France - and Roland Groz - Grenoble Universités, France.

12h30 Lunch

                To unsubscribe, send an empty email to
     mailto:[log in to unmask]
    For further details of CHI lists see