Books

Short works

Books : reviews

Didier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson, eds.
ZB 2002: Formal Specification and Development in Z and B: Second International Conference of B and Z Users, Grenoble.
Springer. 2002

(read but not reviewed)

Contents

Eric C. R. Hehner, Ioannis T. Kassios. Theories, Implementations, and Transformations. 2002
Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Mery, Airy Weinzoepflen. Incremental Proof of the Producer/Consumer Property for the PCI Protocol. 2002
Michael Poppleton, Richard Banach. Controlling Control Systems: An Application of Evolving Retrenchment. 2002
Neil J. Robinson. Checking Z Data Refinements Using an Animation Tool. 2002
Graeme Smith, Florian Kammuller, Thomas Santen. Encoding Object-Z in Isabelle/HOL. 2002
Ian Toyn, Susan Stepney. Characters + Mark-up = Z Lexis. 2002
full paper
Marielle Doche, Andrew M. Gravell. Extraction of Abstraction Invariants for Data Refinement. 2002
Leonid Mikhailov, Michael J. Butler. An Approach to Combining B and Alloy. 2002
Ralph-Johan Back. Software Construction by Stepwise Feature Introduction. 2002
Jim Woodcock, Ana L. C. Cavalcanti. The Semantics of Circus. 2002
Ralph Miarka, John Derrick, Eerke A. Boiten. Handling Inconsistencies in Z Using Quasi-Classical Logic. 2002
Eerke A. Boiten. Loose Specification and Refinement in Z. 2002
Jean-Raymond Abrial, Louis Mussat. On Using Conditional Definitions in Formal Theories. 2002
Steve Dunne. A Theory of Generalised Substitutions. 2002
Sergiy A. Vilkomir, Jonathan P. Bowen. Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing. 2002
Bruno Legeard, Fabien Peureux, Mark Utting. A Comparison of the BTT and TTF Test-Generation Methods. 2002
David Basin, Frank Rittinger, Luca Vigano. A Formal Analysis of the CORBA Security Service. 2002
Jean-Paul Bodeveix, Mamoun Filali. Type Synthesis in B and the Translation of B to PVS. 2002
Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte. "Higher-Order" Mathematics in B. 2002
Pierre Chartier. ABS Project: Merging the Best Practices in Software Design from Railway and Aircraft Industries. 2002
James Blow, Andy Galloway. Generalised Substitution Language and Differentials. 2002
Steve Schneider, Helen Treharne. Communicating B Machines. 2002
Francoise Bellegarde, Jacques Julliand, Olga Kouchnarenko. Synchronized Parallel Composition of Event Systems in B. 2002
Antonis Papatsaras, Bill Stoddart. Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study. 2002
Francoise Bellegarde, Samir Chouali, Jacques Julliand. Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions. 2002
Soon-Kyeong Kim, David Carrington. A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints. 2002
Regine Laleau, Fiona Polack. Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development. 2002

Helen Treharne, Steve King, Martin C. Henson, Steve Schneider, eds.
ZB 2005: Formal Specification and Development in Z and B: Fourth International Conference of B and Z Users, Guildford, UK.
Springer. 2005

(read but not reviewed)

Contents

Cliff B. Jones. Specification before Satisfaction: the case for research into obtaining the right specification. 2005
(invited talk, extended abstract)
Michael Leuschel, Edd Turner. Visualising larger state spaces in ProB. 2005
John Derrick, Heike Wehrheim. Non-atomic refinement in Z and CSP. 2005
Steve Dunne, Stacey Conroy. Process refinement in B. 2005
Petra Malik, Mark Utting. CZT: a framework for Z tools. 2005
Graeme Smith, Luke Wildman. Model checking Z specifications using SAL. 2005
Ian Toyn, Andy Galloway. Proving properties of Stateflow models using ISO Standard Z and CADiZ. 2005
J. Christian Attiogbe. A stepwise development of the Peterson's mutual exclusion algorithm using B Abstract Systems. 2005
Pontus Bostrom, Marina Walden. An extension of Event B for developing Grid systems. 2005
Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial. The challenge of probabilistic Event B. 2005
(invited talk, extended abstract)
Jemima Rossmorris, Susan Stepney. Requirements as conjectures: intuitive DVD menu navigation. 2005
Frank Zeyda, Bill Stoddart, Steve Dunne. A Prospective-Value semantics for the GSL. 2005
Richard Banach, Simon Fraser. Retrenchment and the B-toolkit. 2005
Jean-Raymond Abrial, Dominique Cansell, Dominique Mery. Refinement and reachability in Event B. 2005
Soon-Kyeong Kim, David Carrington. A rigorous foundation for pattern-based design models. 2005
Nuno Amalio, Fiona Polack, Susan Stepney. An object-oriented structuring for Z based on Views. 2005
Yann Zimmermann, Diana Toma. Component reuse in B using ACL2. 2005
Didier Bert, Marie-Laure Potet, Nicolas Stouls. GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties. 2005
Benjamin W. Long. Formal verification of a type flaw attack on a security protocol using Object-Z. 2005
Frederic Badeau, Arnaud Amelot. Using B as a high level programming language in an industrial project: Roissy VAL. 2005
(invited talk)
Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan. Development via refinement in Probabilistic B -- foundation and case study. 2005
Eerke A. Boiten, John Derrick. Formal program development with approximations. 2005
Lindsay Groves. Practical data refinement for the Z schema calculus. 2005
Ingo Bruckner, Heike Wehrheim. Slicing Object-Z specifications for verification. 2005
Fabrice Bouquet, Frederic Dadeau, Julien Groslambert. Checking JML specifications with B Machines. 2005
Judy Bowen, Steve Reeves. Including design guidelines in the formal specification of interfaces in Z. 2005
Abdolbaghi Rezazadeh, Michael J. Butler. Some guidelines for formal development of web-based applications in the B-Method. 2005