7. IFM 2009: Düsseldorf, Germany

Invited Talks

• Thai Son Hoang, Hironobu Kuruma, David A. Basin, Jean-Raymond Abrial:
  Developing Topology Discovery in Event-B. 1-19
  
• Michael Butler:
  Decomposition Structures for Event-B. 20-38
  
• Byron Cook:
  Taming the Unbounded for Hardware Synthesis. 39
  

Contributed Papers

• Jordi Cabot, Robert Clarisó, Daniel Riera:
  Verifying UML/OCL Operation Contracts. 40-55
  
• Peter Y. H. Wong, Jeremy Gibbons:
  Property Specifications for Workflow Modelling. 56-71
  
• Thang H. Bui, Albert Nymeyer:
  Formal Verification Based on Guided Random Walks. 72-87
  
• Jan Stöcker, Frédéric Lang, Hubert Garavel:
  Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. 88-102
  
• Steve Schneider, Helen Treharne:
  Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B. 103-117
  
• Robert Colvin, Ian J. Hayes:
  CSP with Hierarchical State. 118-135
  
• Benjamin Weiß:
  Predicate Abstraction in a Program Logic Calculus. 136-150
  
• Frank Zeyda, Ana Cavalcanti:
  Mechanised Translation of Control Law Diagrams into Circus. 151-166
  
• Gwen Salaün, Tevfik Bultan:
  Realizability of Choreographies Using Process Algebra Encodings. 167-182
  
• Eerke A. Boiten, John Derrick:
  Modelling Divergence in Relational Concurrent Refinement. 183-199
  
• Sebastian Voss, Maria Sorea, Klaus Echtle:
  SAL-Based Symbolic Scheduling in Time-Triggered Networks. 200-214
  
• Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen:
  Incremental Reasoning for Multiple Inheritance. 215-230
  
• Abigail Parisaca Vargas, Ana Gabriela Garis, S. Lizeth Tapia Tarifa, Chris George:
  Model Checking LTL Formulae in RAISE with FDR. 231-245
  
• Ralf Lämmel, Vadim Zaytsev:
  An Introduction to Grammar Convergence. 246-260
  
• Zarrin Langari, Richard J. Trefler:
  Application of Graph Transformation in Verification of Dynamic Systems. 261-276
  
• Osman Hasan, Naeem Abbasi, Sofiène Tahar:
  Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays. 277-291
  
• Gordon J. Pace, Gerardo Schneider:
  Challenges in the Specification of Full Contracts. 292-306
  
• Nikola Benes, Lubos Brim, Ivana Cerná, Jiri Sochor, Pavlína Vareková, Barbora Zimmerova:
  Partial Order Reduction for State/Event LTL. 307-321
  
• Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu:
  Dynamic Path Reduction for Software Model Checking. 322-336
  
• Jérémy Milhau, Benoît Fraikin, Marc Frappier:
  Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions. 337-351
  
• Astrid Rakow:
  Decompositional Petri Net Reductions. 352-366