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