FM 2008

Technical Symposium

A selection of five invited talks and 23 outstanding research papers provides the opportunity to learn about the newest developments in the theory and application of formal methods. The program (detailed below) covers a wide range of topics, including real-time and concurrency, design, verification, communication, runtime monitoring and analysis, constraint analysis, programming language analysis, formal methods practice, and grand challenge problems.

The best paper award has been won by Annabelle McIver, Carroll Morgan and Carlos Gonzalía for their paper "Proofs and refutations for probabilistic systems". You can see here a scan of their diploma.

Wednesday, May 28
8:00-9:00 Registration desk open.
9:00-10:00 Welcome
Invited speaker:
Arvind, Getting Formal Verification into Design Flow
10:00-10:30 Coffee Break

CoVaC: Compiler Validation by Program Analysis of the Cross-Product
Anna Zaks and Amir Pnueli

Lazy Behavioral Subtyping
Johan Dovland, Einar Broch Johnsen, Olaf Owe and Martin Steffen

Checking well-formedness of pure-method specifications
Arsenii Rudich, Adam Darvas and Peter Müller
Industry Day
12:00-13:30 Lunch
Tool & Posters Session,
Book Exhibition,
Tool Demos
13:30-15:00 VERIFICATION

Verifying Dynamic Pointer-Manipulating Threads
Stefan Rieger and Thomas Noll

Proofs and refutations for probabilistic systems
Annabelle McIver, Carroll Morgan and Carlos Gonzalia

Assume Guarantee Verification for Interface Automata
Michael Emmi, Dimitra Giannakopoulou and Corina Pasareanu
Industry Day
15:00-15:30 Coffee Break

Automated Verification of Dense-Time MTL Specifications via Discrete-Time Approximatio
Carlo Alberto Furia, Matteo Rossi and Matteo Pradella

A Model Checking Language for Concurrent Value-Passing Systems
Radu Mateescu and Damien Thivolle
Industry Day

Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code
Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn and Wolfgang Reif

Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM
Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald

Thursday, May 29
8:00-9:00 Registration desk open.
9:00-10:00 Invited Speaker:
Shmuel Katz, Aspects and Formal Methods
10:00-10:30 Coffee Break
10:30-12:00 FM PRACTICE

Indutrial Use of Formal Methods for a High-Level Security Evaluation
Boutheina Chetali and Quang-Huy Nguyen

Secret Ninja Formal Methods
Joseph Kiniry and Daniel M. Zimmerman

Specification and Checking of Software Contracts for Conditional Information Flow
Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag and David Greve
Tool presentations
12:00-13:30 Lunch
Tool & Posters Session,
Book Exhibition,
Tool Demos
13:30-14:30 Invited speaker:
Paolo Bresciani, The ICT theme in the FP7
14:30-15:00 Coffee Break

JML Runtime Assertion Checking: Improved Error Reporting and Efficiency using Strong Validity
Patrice Chalin and Frédéric Rioux

Provably Correct Runtime Monitoring
Irem Aktug, Mads Dam and Dilian Gurov

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into Lotos
Olivier Ponsini and Wendelin Serwe

A rigorous approach to networking: TCP, from implementation to protocol to service
Tom Ridge, Michael Norrish and Peter Sewell
16:00- 16:00- Excursion & Banquet

Friday, May 30
8:00-9:00 Registration desk open.
9:00-10:00 Invited speaker:
Jayadev Misra, Simulation, Orchestration and Logical Clocks
10:00-10:30 Coffee Break

Constraint Prioritization for Efficient Analysis of Declarative Models
Engin Uzuncaova and Sarfraz Khurshid

Finding Minimal Unsatisfiable Cores of Declarative Specifications
Emina Torlak, Felix Chang and Daniel Jackson

Precise Interval Analysis vs. Parity Games
Thomas Gawlitza and Helmut Seidl
FM education
12:00-13:30 Lunch
Tool & Posters Session,
Book Exhibition,
Tool Demos
13:30-14:30 Invited speaker:
Dawson Engler, Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems
14:30.15:00 Coffee Break
15:00-16:30 DESIGN

Introducing Objects through Refinement
Tim McComb and Graeme Smith

Masking Faults while Providing Bounded-Time Phased Recovery
Borzoo Bonakdarpour and Sandeep Kulkarni

Towards Consistent Specifications of Product Families
Alexander Harhurin and Judith Hartmann
16:30-17:00 Closing -17:00