Invited speakers Program Conference dinner Programme Committee Chairs


FM2009 is the sixteenth symposium in a series of the Formal Methods Europe association. The symposium will be organized as a world congress. Reflecting this global span, the Programme Committee has been recruited from all over the world: it comprises 82 members representing 46 countries. For the Symposium, papers on every aspect of the development and application of formal methods for the improvement of the current practice on system developments were invited for submission. The proceedings of FM2009 will be published as a volume in the Springer Lecture Notes in Computer Science series.

Springer sponsors a Best Paper Award, which will include free electronic access to the Formal Aspects of Computing journal for one year, and a choice of Springer books. In addition a number of reputable journals are expected to publish anniversary special issues, for which authors of a selection of the papers accepted for FM2009 will be invited to submit. This has already been confirmed for the journals Formal Aspects of Computing and Formal Methods in System Design.

Invited speakers


Wednesday, the 4th of November, 2009

09.00 Opening ceremony
09.15 Invited Talk (Chair John Fitzgerald)
Formal Methods for Privacy
Jeannette Wing
10.15 Coffee-break
10.45 Model checking I (Chair Annabelle McIver)
Recursive Abstractions for Parameterized Systems
Joxan Jaffar, Andrew Edward Santosa
Abstract Model Checking without Computing the Abstraction
Stefano Tonetta
Three-Valued Spotlight Abstractions
Jonas Schrieb, Heike Wehrheim, Daniel Wonisch
Fair Model Checking with Process Counter Abstraction
Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong
10.45 Technical session: Compositionality (Chair Peter Gorm Larsen)
Systematic Development of Trustworthy Component Systems
Rodrigo Ramos, Augusto Sampaio, Alexandre Mota
Partial Order Reductions using Compositional Confluence Detection
Frederic Lang, Radu Mateescu
A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition
Ralph Jeffords, Constance Heitmeyer, Myla Archer, Elizabeth Leonard
12.45 Lunch
14.00 Verification (Chair Marc Frappier)
Abstract Specification of the UBIFS File System for Flash Memory
Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
Inferring Mealy Machines
Muzammil Shahbaz, Roland Groz
Formal Management of CAD/CAM Processes
Michael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz
14.00 Technical session: Concurrency (Chair Cliff Jones)
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way
Rik Eshuis
Symbolic Predictive Analysis for Concurrent Programs
Chao Wang, Sudipta Kundu, Malay Ganai, Aarti Gupta
On the Difficulty of Concurrent-System-Design, Illustrated with a 2x2 Switch Case Study
Edgar Daylight, Sandeep Shukla
15.30 Coffee-break
16.00 Invited Talk (Chair Dennis Dams)
What can Formal Methods bring to Systems Biology?
Wan Fokkink

Thursday, the 5th of November, 2009

09.00 Invited Talk (Chair Jozef Hooman)
Guess and Verify - Back to the Future
Colin O'Halloran
10.00 Coffee-break
10.30 Refinement (Chair Michael Butler)
Sums and Lovers: Case studies in security, compositionality and refinement
Annabelle McIver, Carroll Morgan
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing
Neil Walkinshaw, John Derrick, Qiang Guo
Model Checking Linearizability via Refinement
Yang Liu, Wei Chen, Yanhong Liu, Jun Sun
10.30 Static Analysis (Chair Jaco van de Pol)
It's doomed; we can prove it
Jochen Hoenicke, Rustan Leino, Andreas Podelski, Martin Schäf, Thomas Wies
``Carbon Credits'' for Resource-Bounded Computations using Amortised Analysis
Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann
Field-Sensitive Value Analysis by Field-Insensitive Analysis
Elvira Albert, Puri Arenas, Samir Genaim, German Puebla
12.00 Lunch
12.30 FME Business Meeting
13.30 Theorem proving (Chair Lars-Henrik Eriksson)
Making Temporal Logic Calculational: A Tool For Unification and Discovery
Raymond Boute
A Tableau for CTL*
Mark Reynolds
Certifiable specification and verification of C programs
Christoph Lüth, Dennis Walter
Formal Reasoning about Expectation Properties for Continuous Random Variables
Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiene Tahar, Reza Akbarpour
13.30 Semantics (Chair Bernhard Aichernig)
The Denotational Semantics of slotted-Circus
Pawel Gancarski, Andrew Butterfield
Unifying Probability with Nondeterminism
Yifeng Chen, Jeff Sanders
Towards an Operational Semantics for Alloy
Theophilos Giannakopoulos, Daniel Dougherty, Kathi Fisler, Shriram Krishnamurthi
A robust semantics hides fewer errors
Steve Reeves, David Streader
15.30 Coffee-break
16.00 Invited Talk (Chair Jos Baeten)
Verification, Testing and Statistics
Sriram Rajamani
18.30 Conference dinner

Friday, the 6th of November, 2009

09.00 Invited Talk (Chair Ana Cavalcanti)
Security, Probability and Nearly Fair Coins in the Cryptographers' Café
Carroll Morgan
10.00 FM'11
10.15 Coffee-break
10.45 Special Track: industrial applications I (Chair Stefania Gnesi)
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks
Faranak Heidarian, Julien Schmaltz and Frits Vaandrager
Formal Verification of Avionics Software Products
Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study
Andre Platzer, Edmund Clarke
10.15 Coffee-break
10.45 Object-orientation (Chair Heike Wehrheim)
Connecting UML and VDM++ with Open Tool Support
Kenneth Lausdahl, Hans Kristian Agerlund Lintrup, Peter Gorm Larsen
Language and Tool Support for Class and State Machine Refinement in UML-B
Mar Yah Said, Michael Butler, Colin Snook
Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects
Einar Broch Johnsen, Marcel Kyas, Ingrid Yu
Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created
Wolfgang Ahrendt, Frank de Boer and Immo Grabe
12.45 Lunch
14.00 Pointers (Chair Jeff Sanders)
Reasoning about Memory Layouts
Holger Gast
A smooth combination of Linear and Herbrand Equalities for Polynomial Time Must-alias Analysis
Helmut Seidl, Vesal Vojdani, Varmo Vene
14.00 Real-time (Chair Dino Mandrioli)
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery
Borzoo Bonakdarpour, Sandeep Kulkarni
Verifying Real-Time Systems against Scenario-Based Requirements
Kim Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas
15.00 Coffee-break
15.30 Special Track: tools and industrial applications II (Chair Jim Woodcock)
Formal Specification of a Cardiac Pacing System
Artur Gomes, Marcel Oliveira
Automated Property Verification for Large Scale B Models
Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge
Reduced Execution Semantics of MPI: From theory to practice
Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert Kirby
15.30 Model checking II (Chair Marie-Claude Gaudel)
A Metric Encoding for Bounded Model Checking
Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro
An incremental approach to scope-bounded checking using a lightweight formal method
Danhua Shao, Sarfraz Khurshid, Dewayne Perry
Verifying Information Flow Control Over Unbounded Processes
William Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas Reps
Specification and Verification of Web Applications in Rewriting Logic
María Alpuente, Demis Ballis, Daniel Romero
17.30 Closing
John Fitzgerald

Conference dinner

The venue for the conference dinner of FM2009 is the Van Abbemuseum of modern and contemporary art. This internationally renowned museum is in the centre of Eindhoven, within walking distance of both the conference venue and hotels. It has got an interesting hybrid building, consisting of the original red brick museum from 1936 extended with a much larger modernist part from 2003, and is situated on, and partly in, the Dommel river. The dinner will take place in museum restaurant, which has river views, and delegates will be able to explore the collection and building of the museum before dinner, with the opportunity to take guided tours in small groups.


PC Chairs

General Chair