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.
| 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 |
| 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 |
| 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 |
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.