author : Helen Treharne

Contents

• Cliff B. Jones.

Specification before Satisfaction: the case for research into obtaining the right specification

(invited talk, extended abstract)

• Michael Leuschel, Edd Turner.

Visualising larger state spaces in ProB

• John Derrick, Heike Wehrheim.

Non-atomic refinement in Z and CSP

• Steve Dunne, Stacey Conroy.

Process refinement in B

• Petra Malik, Mark Utting.

CZT: a framework for Z tools

• Graeme Smith, Luke Wildman.

Model checking Z specifications using SAL

• Ian Toyn, Andy Galloway.

Proving properties of Stateflow models using ISO Standard Z and CADiZ

• J. Christian Attiogbe.

A stepwise development of the Peterson's mutual exclusion algorithm using B Abstract Systems

• Pontus Bostrom, Marina Walden.

An extension of Event B for developing Grid systems

• Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial.

The challenge of probabilistic Event B

(invited talk, extended abstract)

• Jemima Rossmorris, Susan Stepney.

Requirements as conjectures: intuitive DVD menu navigation

• Frank Zeyda, Bill Stoddart, Steve Dunne.

A Prospective-Value semantics for the GSL

• Richard Banach, Simon Fraser.

Retrenchment and the B-toolkit

• Jean-Raymond Abrial, Dominique Cansell, Dominique Mery.

Refinement and reachability in Event B

• Soon-Kyeong Kim, David Carrington.

A rigorous foundation for pattern-based design models

• Nuno Amalio, Fiona Polack, Susan Stepney.

An object-oriented structuring for Z based on Views

• Yann Zimmermann, Diana Toma.

Component reuse in B using ACL2

• Didier Bert, Marie-Laure Potet, Nicolas Stouls.

GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties

• Benjamin W. Long.

Formal verification of a type flaw attack on a security protocol using Object-Z

• Frederic Badeau, Arnaud Amelot.

Using B as a high level programming language in an industrial project: Roissy VAL

(invited talk)

• Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan.

Development via refinement in Probabilistic B -- foundation and case study

• Eerke A. Boiten, John Derrick.

Formal program development with approximations

• Lindsay Groves.

Practical data refinement for the Z schema calculus

• Ingo Bruckner, Heike Wehrheim.

Slicing Object-Z specifications for verification

• Fabrice Bouquet, Frederic Dadeau, Julien Groslambert.

Checking JML specifications with B Machines

• Judy Bowen, Steve Reeves.

Including design guidelines in the formal specification of interfaces in Z

• Abdolbaghi Rezazadeh, Michael J. Butler.

Some guidelines for formal development of web-based applications in the B-Method