Programme
Wednesday Thursday Friday
Wednesday 13th April
| 8:30 |
Registration |
| 9:20 |
Welcome |
| 9:30 |
Invited talk: Cliff Jones |
| 10:30 |
Visualising Larger State Spaces in ProB |
Michael Leuschel,
Ed Turner |
| 11:00 |
Break |
| 11:30 |
Refinement |
| |
Non-atomic refinement in Z and CSP |
John Derrick,
Heike Wehrheim |
| |
Process refinement in B |
Steve Dunne,
Stacey Conroy |
| 12:30 |
Lunch |
| 14:00 |
Tools |
| |
CZT---A Framework for Z Tools |
Petra Malik,
Mark Utting |
| |
Model checking Z specifications using SAL |
Graeme Smith,
Luke Wildman |
| |
Proving Properties of Stateflow Models using ISO Standard Z and CADiZ |
Ian Toyn,
Andy Galloway |
| 15:30 |
Break |
| 16:00 |
Case studies |
| |
A Stepwise Development of the Peterson's Mutual
Exclusion Algorithm Using B Abstract Systems |
J. Christian Attiogbé |
| |
An extension of Event B for developing grid systems |
Pontus Boström,
Marina Waldén |
| 17:00 |
Close |
| 19:00 |
Guildford Guildhall reception |
Thursday 14th April
| 9.00am |
FME and BCS-FACS Invited talk: Carroll Morgan |
| 10:00 |
Requirements as conjectures: intuitive DVD menu navigation |
Jemima Rossmorris,
Susan Stepney |
| 10:30 |
Break |
| 11:00 |
Theory and tools |
| |
A Prospective-value Semantics for the GSL |
Frank Zeyda,
Bill Stoddart,
Steve Dunne |
| |
Retrenchment and the B-Toolkit |
Richard Banach,
Simon Fraser |
| |
Refinement and Reachability in Event_B |
Jean-Raymond ABRIAL,
Dominique Cansell,
Dominique Méry |
| 12:30 |
Lunch |
| 14:00 |
Object orientation |
| |
A Rigorous Foundation for Pattern Based Design Models |
Soon-Kyeong Kim,
David Carrington |
| |
An Object-Oriented Structuring for Z based on Views |
Nuno Amalio,
Fiona Polack,
Susan Stepney
|
| |
Component reuse in B using ACL2 |
Yann Zimmermann,
Diana Toma |
| 15:30 |
Break |
| 16:00 |
Security applications |
| |
GeneSyst: a tool to reason about behavioral
aspects of B event specifications. Application to security properties |
Didier Bert,
Marie-Laure Potet,
Nicolas Stouls |
| |
Formal Verification of a Type Flaw Attack on a Security Protocol using Object-Z |
Benjamin Long |
| 17:00 |
Close |
| 18:15 |
Set off for dinner at Loseley Park |
Friday 15th April
| 9.00 |
Invited talk: Frédéric Badeau |
| 10:00 |
Development via Refinement in Probabilistic B
--- Foundation and Case Study |
Thai Son Hoang,
Zhendong Jin,
Ken Robinson,
Carroll Morgan,
Annabelle McIver |
| 10:30 |
Break |
| 11:00 |
Theory |
|
Formal Program Development with Approximations |
Eerke Boiten,
John Derrick |
| |
Practical Data Refinement for the Z Schema Calculus |
Lindsay Groves |
| |
Slicing Object-Z specifications for verification |
Ingo Brückner,
Heike Wehrheim |
| 12:30 |
Lunch |
| 14:00 |
Development |
| |
Checking JML specifications with B
machines |
Fabrice Bouquet,
Frédéric Dadeau,
Julien Groslambert |
| |
Including Design Guidelines in the Formal Specification of Interfaces in Z |
Judy Bowen,
Steve Reeves |
| |
Some Guidelines for Formal Development of
Web-based Applications in B-Method |
Abdolbaghi Rezazadeh,
Michael Butler |
| 15:30 |
Close (and prizes) |
|
|
