Wednesday, August 23 |
||
| 8:45 - 9:00 | Opening Remarks MDCL 1105 |
|
| 9:00 - 10:00 |
Invited Talk
Session Chair: Steve SchneiderMDCL 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 HehnerMDCL 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 FarmerMDCL 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 FitzgeraldMDCL 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 LeroyMDCL 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 |
|
Technical Symposium
All sessions are in Michael DeGroote Centre
for Learning, MDCL.