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
|
| 10:30-12:00 |
PROGRAMMING LANGUAGE ANALYSIS
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 |
| 15:30-16:30 |
REAL-TIME AND CONCURRENCY
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 |
| 16:30-17:30 |
GRAND CHALLENGE PROBLEMS
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 |
| 15:00-16:00 |
RUNTIME MONITORING AND ANALYSIS
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
|
COMMUNICATION
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
|
| 10:30-12:00 |
CONSTRAINT ANALYSIS
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
|
|
News
- Pictures from the conference week now available. (2.7.2008)
- Material for the IDay presentations available. (4.6.2008)
- The diploma for the best paper award is on the web. (4.6.2008)
- The
link to the next Formal Methods conference has been added. (4.6.2008)
- The abstract of Paolo Bresciani is now available. (23.5.2008)
- The registration is now closed. (22.5.2008)
- The program of the Doctoral Symposium is now
available. (15.5.2008)
- Unfortunately, Tutorial 7 has been
cancelled. (9.5.2008)
- Comparing the hotels in Turku by
a non-profit organisation can be found here. (9.5.2008)
- A list of selected restaurants, pubs and cafés can now be found here. (9.5.2008)
- Hostel Turku added as new accommodation alternative. Please check the
accommodation page for more information. (15.4.2008)
- The abstract of Prof. Arvind is now
accessible. (11.4.2008)
Archive
|
