FM 2006

 
August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006

 

Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006


Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chairs

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel


Technical Symposium

All sessions are in Michael DeGroote Centre for Learning, MDCL.

Wednesday, August 23
8:45 - 9:00
Opening Remarks
MDCL 1105
9:00 - 10:00
Invited Talk
Session Chair: Steve Schneider
MDCL 1105

Tom Henzinger. Embedded Systems Design Challenge.
10:00 - 10:30
Break
10:30 - 12:30
Industry Day
MDCL 1105
Interactive Theorem Proving
Session Chair: Tobias Nipkow
MDCL 1110

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg and Wolfgang Reif. The Mondex Challenge: Machine Checked Proofs for an Electronic Purse

Jonathan Schmitt, Alwin Hoffmann, Michael Balser, Wolfgang Reif and Mar Marcos. Interactive Verification of Medical Guidelines

David Delahaye, Jean-Frédéric Étienne and Véronique Viguié Donzeau-Gouge. Certifying Airport Security Regulations using the Focal Environment

Shinya Umeno and Nancy Lynch. Proving safety properties of an aircraft landing protocol using I/O Automata and the PVS theorem prover: a case study
12:30 - 14:00
Lunch
14:00 - 15:00
Invited Talk
Session Chair: Eric Hehner
MDCL 1105

Ernie Cohen: Validating the Microsoft Hypervisor
15:00 - 15:30
Break
15:30 - 17:30
Industry Day
MDCL 1105
Modeling
Session Chair: Dominique Mery
MDCL 1110

Kim G. Larsen, Ulrik Nyman and Andrzej Wasowski. Interface Input/Output Automata

Greg Brunet, Marsha Chechik and Sebastian Uchitel. Properties of Behavioural Model Merging

Angela Freitas and Ana Lucia Caneca Cavalcanti. Automatic translation from Circus to Java

Annabelle McIver. Quantitative refinement and model checking for the analysis of probabilistic systems
 
Thursday, August 24
9:00 - 10:00
Invited Talk
Session Chair: Bill Farmer
MDCL 1105

Nick Griffin: Bertrand Russell: A Philosophy for Formal Methods and a Formal Method for Philosophy
10:00 - 10:30
Break
10:30 - 12:30
Real Time and Industrial Experience
Session Chair: Pamela Zave
MDCL 1105

Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++

Jewgenij Botaschanjan, Alexander Gruler, Alexander Harhurin, Leonid Kof, Maria Spichkova and David Trachtenherz. Towards Modularized Verification of Distributed Time-Triggered Systems

Stefano Bacherini, Alessandro Fantechi, Matteo Tempestini and Niccolň Zingoni. A Story about Formal Methods Adoption by a Railway Signaling Manufacturer

Yujun Zheng, Jinquan Wang and Kan Wang. Partially Introducing Formal Methods into Object-Oriented Development: case studies using a metrics-driven approach
Specification and Refinement
Session Chair: Tom Maibaum
MDCL 1110

Tim McComb and Graeme Smith. Compositional Class Refinement in Object-Z

Neil Evans and Michael Butler. A Proposal for Records in Event-B

José Nuno Oliveira and Cesar Jesus Rodrigues. Pointfree Factorization of Operation Refinement

Nuno Amálio, Susan Stepney and Fiona Polack. A Formal Template Language enabling Metaproof
12:30 - 14:00 Lunch
14:00 - 15:00
Programming Languages
Session Chair: Emil Sekerinski
MDCL 1105

Ioannis Kassios. Dynamic Frames: Support for Framing, Dependencies and Sharing without Restrictions

Alcino Cunha, José Nuno Oliveira and Joost Visser. Type-safe Two- level Data Transformation
Algebra & Education
Session Chair: Wolfram Kahl
MDCL 1110

Peter Hofner, Bernhard Moeller and Ridha Khedri. Feature Algebras

Raymond Boute. Using Domain Independent Problems for Introducing Formal Methods
15:00 -
Excursion and Banquet

David Parnas. Formal Methods for Dinner Engineering (after dinner speech)
 
Friday, August 25
9:00 - 10:00
Invited Talk
Session Chair: John Fitzgerald
MDCL 1105

Peter Lindsay: Distributed Control in Network-Based Systems
10:00 - 10:30
Break
10:30 - 12:30
Modeling
Session Chair: Juergen Dingel
MDCL 1105

Pamela Zave. Compositional Binding in Network Domains

Zarrin Langari and Richard Trefler. Formal Modeling of Communication Protocols By Graph Transformations

Marc Aiguier, Karim Berkani and Pascale Le Gall. Feature specification and static analysis for interaction resolution

Mass Soldal Lund and Ketil Stølen. A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice
Java & Testing
Session Chair: George Necula
MDCL 1110

Xin Li, Jim Hoover and Piotr Rudnicki. Towards Automatic Exception Safety Verification

Cyrille Valentin Artho, Armin Biere and Shinichi Honiden. Enforcer -- Efficient Failure Injection

Frederic Dadeau, Fabrice Bouquet and Bruno Legeard. Automated Boundary Test Generation from JML Specifications

Wojciech Mostowski. Formal Reasoning about Non-Atomic Java Card Methods in Dynamic Logic
12:30 - 14:00
Lunch
14:00 - 15:00
Invited Talk
Session Chair: Xavier Leroy
MDCL 1105

George Necula: Data Structure Specifications via Local Equality Axioms
15:00 - 15:30
Break
15:30 - 17:30
Programming Lanugages
Session Chair: Ana Cavalcanti
MDCL 1105

Sandrine Blazy, Zaynah Dargaye and Xavier Leroy. Formal verification of a C compiler front-end

Thuan Quang Huynh and Abhik Roychoudhury. A Memory Model Sensitive Checker for C#

Fabian Bannwart and Peter Müller. Changing Programs Correctly: Refactoring with Specifications

Viorel Preoteasa. Mechanical Verification of Recursive Procedures Manipulating Pointers using Separation Logic
Model Checking
Session Chair: Marsha Chechik
MDCL 1110

Wendy Johnston, Kirsten Winter, Lionel van den Berg, Paul Strooper and Peter Robinson. Model-based Variable and Transition Orderings for efficient Symbolic Model Checking

Alastair F. Donaldson and Alice Miller. Exact and Approximate Strategies for Symmetry Reduction in Model Checking

Alexandre Genon, Thierry Massart and Cédric Meuter. Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences is Needed to Model-Check Traces

Aleksandr Zaks and Amir Pnueli. PSL Model Checking and Run-time Verification via Testers
17:30 - 17:45
Closing Remarks
MDCL 1105