Programme iFM 2009

Download Programme as PDF (now includes workshops and tutorials)
Also, see the LNCS proceedings, with contents available online.

Monday, 16. February

08:30 - 9:30 Registration

9:00 - Tutorial Contract Specification and Checking: Application to .NET and C

9:30 - FMSOA and IMFMT Workshops

Tuesday, 17. February

09:00 Opening

09:00-10:00 Invited speaker

  • Byron Cook:
    Taming the unbounded for hardware synthesis

10:00-10:30 Coffee

10:30 -12:00 Verification I (Session chair: Martin Fränzle)

  • Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiaowan Huang, Scott Smolka, Radu Grosu:
    Dynamic Path Reduction for Software Model Checking
  • Nikola Benes, Lubos Brim, Ivana Cerna, Jiri Sochor, Pavlina Varekova, Barbora Zimmerova:
    Partial Order Reduction for State/Event LTL
  • Astrid Rakow:
    Decompositional Petri Net Reductions

12:00-14:00 Lunch

14:00-15:30 Time & Probability (Session chair: Stephan Merz)

  • Jan Stöcker, Frederic Lang, Hubert Garavel:
    Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format
  • Sebastian Voss, Maria Sorea:
    SAL-Based Symbolic Scheduling in Time-Triggered Networks
  • Osman Hasan, Naeem Abbasi, Sofiene Tahar:
    Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays

15:30 - 16:00 Coffee

16:00-17:30 Process Algebras (Session chair: Kenji Taguchi)

  • Peter Wong, Jeremy Gibbons:
    Property Specifications for Workflow Modelling
  • Gwen Salaün, Tevfik Bultan:
    Realizability of Choreographies using Process Algebra Encodings
  • Robert Colvin, Ian Hayes:
    CSP with Hierarchical State

18:00 - 19:30 Bus tour through Düsseldorf and transfer to Rheinturm

19:30 - Conference Dinner at the Rheinturm

Wednesday, 18. February

09:00-10:00 Invited speaker

  • Michael Butler:
    Decomposition structures for Event-B

10:00-10:30 Coffee

10:30-12:00 Refinement (Session chair: Stefan Hallerstede)

  • Steve Schneider, Helen Treharne:
    A new refinement strategy for CSP||B: changing system interfaces consis- tently
  • Eerke Boiten, John Derrick:
    Modelling divergence in Relational Concurrent Refinement
  • Frank Zeyda, Ana Cavalcanti:
    Mechanised Translation of Control Law Diagrams into Circus

12:00-14:00 Lunch

14:00-15:30 Verification II (Session chair: Dominique Méry)

  • Abigail Parisaca Vargas, Ana G. Garis, S. Lizeth Tapia Tarifa, Chris George:
    Model checking LTL formulae in RAISE with FDR
  • Thang Bui, Albert Nymeyer:
    Formal Verification Based on Guided Random Walks
  • Benjamin Weiss:
    Predicate Abstraction in a Program Logic Calculus

15:30 - 16:00 Coffee

16:00 - 17:30 Verification III (Session chair: Helen Treharne)

  • Ralf Laemmel, Vadim Zaytsev:
    An Introduction to Grammar Convergence
  • Zarrin Langari, Richard Trefler:
    Application of Graph Transformation in Verification of Dynamic Systems
  • Jeremy Milhau, Benoit Fraikin, Marc Frappier:
    Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions

19:00 - 20:00 Guided evening tour at the Aquazoo

Thursday, 19. February

09:00-10:00 Invited speaker

  • David Basin:
    Developing Topology Discovery in Event-B

10:00-10:30 Coffee

10:30-12:30 Contracts & Inheritance (Session chair: Heike Wehrheim)

  • Gordon Pace, Gerardo Schneider:
    Challenges in the Specification of Full Contracts
  • Jordi Cabot, Robert Claris, Daniel Riera:
    Verifying UML/OCL Operation Contracts
  • Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen:
    Incremental Reasoning for Multiple Inheritance

12:30 Closing Session

12:30-14:00 Lunch