|
Programme
|
Sunday 1st July
|
|
19.00
|
Early Registration and Welcome
|
|
Tuesday 3rd July
|
|
08.30
|
Registration
|
|
|
MeMoT Workshop
|
|
KeY Tutorial (morning only)
|
|
09.00
|
Jim Woodcock
Unifying Theories of Undefinedness
(Invited talk)
|
|
09.45
|
Andrew Butterfield, Adnan Sherif, and Jim Woodcock
Slotted Circus
|
|
10.15
|
Michael Anthony Smith and Jeremy Gibbons
Unifying Theories of Objects
|
|
10.45
|
Coffee
|
|
11.15
|
Yifeng Chen
Inheriting Laws for Processes with States
|
|
11.45
|
Steve Dunne and Andy Galloway
Lifting General Correctness into Partial Correctness is ok
|
|
12.15
|
Damien Karkinsky, Steve Schneider, and Helen Treharne
Combining Mobility with State
|
|
12.45
|
Lunch
|
|
13.45
|
Johannes Faber, Swen Jacobs, and Viorica
Sofronie-Stokkermans
Verifying CSP-OZ-DC Specifications with Complex Data Types and
Timing Parameters
|
|
14.15
|
Nazareno Aguirre, German Regis, and Tom Maibaum
Verifying Temporal Properties of CommUnity Designs
|
|
14.45
|
Mihaela Gheorghiu, Arie Gurfinkel and Marsha Chechik
Finding State Solutions to Temporal Logic Queries
|
|
15.15
|
Tea
|
|
15.45
|
Christie Marr
Adding Further Conflict and Confusion to CSP
|
|
16.15
|
Tobe Toben
Non-Interference Properties for Data-Type Reduction of
Communicating Systems
|
|
16.45
|
John Derrick, Gerhard Schellhorn, and Heike Wehrheim
Proving Linearizability via Non-atomic Refinement
|
|
17.30
|
IFM reception at the
University Museum
|
|
Wednesday 4th July
|
|
09.00
|
Daniel Jackson
Recent Advances in Alloy
(Invited talk)
|
|
09.45
|
Rodion Podorozhny, Sarfraz Khurshid, Dewayne Perry, and Xiaoqin Zhang
Verification of Multi-agent Negotiations using the Alloy Analyzer
|
|
10.15
|
Daniel Plagge and Michael Leuschel
Validating Z Specifications using the ProB Animator and Model Checker
|
|
10.45
|
Coffee
|
|
11.15
|
Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System
|
|
11.45
|
Hendrik Post and Wolfgang Kuchlin
Integrated Static Analysis for Linux Device Driver Verification
|
|
12.15
|
Dominik Haneberg, Holger Grandy, Wolfgang Reif, and Gerhard Schellhorn
Verifying Smart Card Applications: An ASM Approach
|
|
12.45
|
Lunch
|
|
13.45
|
Daniel Sinnig, Patrice Chalin, and Ferhat Khendek
Common Semantics for Use Cases and Task Models
|
|
14.15
|
Chiara Braghin, Natasha Sharygina, and Katerina Barone-Adesi
Automated Verification of Security Policies in Mobile Code
|
|
14.45
|
Oliver Au, Roger Stone, and John Cooke
Precise Scenarios - A Customer-Friendly Foundation for Formal Specifications
|
|
15.15
|
Tea
|
|
15.45
|
Jean-Francois Couchot and Frederic Dadeau
Guiding the Correction of Parameterized Specifications
|
|
16.15
|
Bjorn Metzler
Decomposing Integrated Specifications for Verification
|
|
16.45
|
Jens Calame, Natalia Ioustinova, Jaco van de Pol, and Natalia Sidorova
Bug Hunting with False Negatives
|
|
18.30
|
Drinks reception and conference dinner
|
|
Thursday 5th July
|
|
09.00
|
Mike Barnett
The Design of the Spec# Programming System
(Invited talk)
|
|
09.45
|
Martijn Oostdijk, Vlad Rusu, Jan Tretmans, Rene de Vries,
and Tim Willemse
Integrating Verification, Testing, and Learning for
Cryptographic Protocols
|
|
10.15
|
Robert Colvin, Lars Grunske, and Kirsten Winter
Probabilistic Timed Behavior Trees
|
|
10.45
|
Coffee
|
|
11.15
|
Jifeng He
UTP Semantics for Web Services
(Invited talk)
|
|
12.00
|
Stefan Hallerstede and Thai Son Hoang
Qualitative Probabilistic Modelling in Event-B
|
|
12.30
|
Osman Hasan and Sofiene Tahar
Verification of Probabilistic Properties in the HOL Theorem Prover
|
|
13.00
|
Lunch
|
|
13.45
|
Marcel Verhoef, Peter Visser, Jozef Hooman, and Jan Broenink
Co-simulation of Distributed Embedded Real-time Control Systems
|
|
14.15
|
Ingo Bruckner
Slicing Concurrent Real-Time System Specifications for Verification
|
|
14.45
|
Larissa Meinicke and Graeme Smith
A Stepwise Development Process for Reasoning about the
Reliability of Real-time Systems
|
|
15.15
|
Tea
|
|
15.45
|
Ansgar Fehnker, Lodewijk van Hoesel, Angelika Mader
Modelling and Verification of the LMAC Protocol for Wireless
Sensor Networks
|
|
16.15
|
Gwen Salaan, Jeff Kramer, Frederic Lang, and Jeff Magee
Translating FSP into LOTOS and Networks of Automata
|
|
16.45
|
Alessandra Cavarra and James Welch
Behavioural Specifications from Class Models
|
|
