author : Martin C. Henson

Books

• Elements of Functional Languages. 1987
• ZB 2002. 2002, with Didier Bert, Jonathan P. Bowen, Ken Robinson
• ZB 2005. 2005, with Helen Treharne, Steve King, Steve Schneider

Short works

• A Logic for the Schema Calculus. 1998. (In ZUM '98 )
• Program Development and Specification Refinement in the Schema Calculus. 2000. (In ZB 2000 )
• An Analysis of forward simulation data refinement. 2003. (In ZB 2003 )
• Operation refinement and monotonicity in the schema calculus. 2003. (In ZB 2003 )

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