Tutorials (2h30)

• Logics, Automata, and Behavioural Properties of Discrete Event Systems,
  by André Arnold (LaBRI, Bordeaux, France). [ slides ]
• Formal Verification of Stochastic Systems,
  by Christel Baier (Univ. Bonn, Germany). [ slides ]
• Software Model Checking via Static and Dynamic Program Analysis,
  by Patrice Godefroid (Bell Labs, Lucent, IL, USA). [ slides A | slides B ]
• Modeling and Analysis of Hybrid Control Systems,
  by Karl H. Johansson (KTH, Stockholm, Sweden). [ slides ]
• Formal Verification of Cryptographic Protocols,
  by Steve Kremer (LSV, Cachan, France). [ slides ]
• From Logic to Games,
  by Igor Walukiewicz (LaBRI, Bordeaux, France). [ slides A | slides B ]

Technical Talks (1h30)

• Verification of Infinite State Probabilistic Systems,
  by Antonín Kučera (MUNI, Brno, Czech Republic).
• Model Checking with Message Sequence Charts,
  by Doron A. Peled (Univ. Warwick, United Kingdom). [ slides ]
• Controller Synthesis and Implementability Issues,
  by Jean-François Raskin (ULB, Brussels, Belgium). [ slides ]
• Formal Methods and Reliability Engineering,
  by Antoine Rauzy (IML, Marseille, France).
• Testing, Optimization and Games,
  by Mihalis Yannakakis (Univ. Columbia, NY, USA). [ slides ]

Roundtable Debate (2h)

• Difficulty to transfer academic results to industrial technologies.
• Which are true needs for the engineers in terms of formal methods?
• Need for the companies as Master degree students or PhD in formal methods?

• Christian Benac (Airbus France, Toulouse, France).
• Thomas Doumenc (Dassault Systèmes, Saint-Cloud, France).
• Bernard Joseph (Thales Systèmes Aéroportés, Bordeaux, France).
• Gérard Ladier (Aerospace Valley/Airbus France, Toulouse, France).
• Bertrand Tavernier (CRIL Technology, Velizy, France).
• Jean-Pierre Velu (SAGEM, Paris, France).

Printer-friendly version