zb2005 logo

4th International Conference
of B and Z Users

University of Surrey, Guildford, UK, 13-15 April 2005
Organised by APCB and the Z User Group


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)





University of Surrey logo Maintained by Rob Delicata.