Monday August 27

09:15 Opening
09:30 Invited Speaker: Dimitria Giannakopoulou, NASA Ames, USA

10:30 Coffee break

11:00 Session 1: Real-time 1
chair: Ralf Pinger
  • Vlad Popa and Wolfgang Schwitzer
    Optimizing the Robustness of Software against Communication Latencies in Distributed Reactive Embedded Systems
  • Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp
    Waiting for locks: How long does it usually take?
  • Victor Bandur, Wolfram Kahl and Alan Wassyng
    Microcontroller Assembly Synthesis from Timed Automaton Task Specifications
12:30 Lunch

14:00 Session 2: Tools
chair: Dimitra Giannakopoulou
  • Jiri Slaby, Jan Strejcek and Marek Trtík
    Checking Properties Described by State Machines:
    On Synergy of Instrumentation, Slicing, and Symbolic Execution
  • Konrad Siek and Paweł T. Wojciechowski
    A Formal Design of a Tool for Static Analysis of Upper Bounds on Object Calls in Java
  • Jiri Barnat, Lubos Brim, Petr Rockai, Jan Beran and Tomas Kratochvila
    Partial Tool Chain to support Automated Formal Verification of Avionics Simulink Designs
15:30 Coffee break

16:00 Session 3: Case studies
chair: Marielle Stoelinga
  • Sjoerd Cranen
    Model checking the FlexRay startup phase
  • Rainer Droste, Christoph Läsche, Cilli Sobiech, Eckard Böde and Axel Hahn
    Model-based Risk Assessment Supporting Development of HSE Plans for Safe Offshore Operations
17:00 End of day I

19:30 FMICS workshop dinner

Tuesday August 28

09:15 Opening of Day II
09:30 Invited Speaker: Hubert Garavel, INRIA Grenoble Rhone-Alpes, France

10:30 Coffee break

11:00 Session 4: software verification
chair: Hubert Garavel
  • Elvira Albert, Bjarte M. Østvold and José Miguel Rojas
    Automated Extraction of Abstract Behavioural Models from JMS Applications
  • Edd Barrett and Andy King
    Range Analysis of Binaries with Minimal Effort
  • Nicolas Ayache, Roberto Amadio and Yann Regis-Gianas
    Certifying and reasoning on cost annotations in C programs
12:30 Lunch

14:00 Session 5: Software Verification / Real-time 2
chair: Radu Mateescu
  • Loic Correnson and Julien Signoles
    Combining Analyses for C Program Verification
  • Nouha Abid, Silvano Dal Zilio and Didier Le Botlan
    Real-Time Specification Patterns and Tools
  • Luca Ferrucci, Matteo Rossi, Dino Mandrioli and Angelo Morzenti
    Modular Automated Verification of Flexible Manufacturing Systems with Metric Temporal Logic and Non-standard analysis
15:30 Closing and Coffee break

15:30 ERCIM meeting

17:30 End of day II