Books
Short works
- The Value of Verification: Positive Experience of Industrial Proof. 1999. (In FM'99 volume 2 )
- Typechecking Z. 2000. (In ZB 2000 )
- Typeconstrained Generics for Z. 2000. (In ZB 2000 )
Books : reviews
Jonathan P. Bowen, Steve Dunne, Andy Galloway, Steve King, eds.
ZB 2000: Formal Specification and Development in Z and B: First International Conference of B and Z Users, York.
Springer. 2000
(read but not reviewed)
Contents
- Soon-Kyeong Kim, David Carrington. A Formal Mapping between UML models and Object-Z Specifications. 2000
- Regine Laleau, Amel Mammar. A Generic Process to Refine a B Specification into a Relational Database Implementation. 2000
- Graeme Smith. Recursive Schema Definitions in ObjectZ. 2000
- Ian Toyn, Samuel H. Valentine, David A. Duffy. On Mutually Recursive Free Types in Z. 2000
- David A. Duffy, Ian Toyn. Reasoning Inductively about Z Specifications via Unification. 2000
- Ken Robinson. Reconciling Axomatic and Modelbased Specifications Using the B Method. 2000
- Theo Dimitrakos, Juan C. Bicarregui, Brian Matthews, Thomas S. E. Maibaum. Compositional structuring in the B Method: A Logical Viewpoint of the Static Context. 2000
- Pierre Bontron, Marie-Laure Potet. Automatic Construction of Validated B components from Structured Developments. 2000
- Dominique Cansell, Dominique Mery. Playing with abstraction and refinement for managing features interactions. 2000
- Mark d'Inverno, Koen Hindriks, Michael Luck. A Formal Architecture for the 3APL Agent Programming Language. 2000
- Helen Treharne, Steve Schneider. How to drive a B Machine. 2000
- Nestor Lopez, Marianne Simonot, Veronique Viguie Donzeau-Gouge. Deriving Software Specifications from Event Based Models. 2000
- Francoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko. Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants. 2000
- Samuel H. Valentine, Ian Toyn, Susan Stepney, Steve King. Typeconstrained Generics for Z. 2000
- full paper
- Ian Toyn, Samuel H. Valentine, Susan Stepney, Steve King. Typechecking Z. 2000
- full paper
- Ralph Miarka, Eerke A. Boiten, John Derrick. Guards, Preconditions and Refinement in Z. 2000
- Richard Banach, Michael Poppleton. Retrenchment, Refinement and Simulation. 2000
- Michael J. Butler, Mairead Meagher. Performing Algorithmic Refinement before Data Refinement in B. 2000
- Martin C. Henson, Steve Reeves. Program Development and Specification Refinement in the Schema Calculus. 2000
- Jean-Louis Lanet. Are Smart Cards the Ideal Domain for Applying Formal Methods?. 2000
- Susan Stepney, David Cooper. Formal Methods for Industrial Products. 2000
- full paper
- Bill Stoddart. An Execution Architecture for GSL. 2000
- Wolfgang Grieskamp. A Computation Model for Z Based on Concurrent Constraint Resolution. 2000
- Rob D. Arthan. Analysis of Compiled Code: A Prototype Formal Model. 2000
- David Cooper, Susan Stepney. Segregation with Communication. 2000
- full paper
- David A. Duffy, Juergen Giesl. Closure Induction in a Z-like Language. 2000
- Chris Matthews, Paul A. Swatman. Fuzzy Concepts and Formal Methods: A Fuzzy Logic Toolkit for Z. 2000
Didier Bert, Jonathan P. Bowen, Steve King, Marina Walden, eds.
ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users, Turku, Finland.
Springer. 2003
(read but not reviewed)
Contents
- Daniel Jackson. Alloy: A Logical Modelling Language. 2003
- (abstract, invited talk)
- Susan Stepney, Fiona Polack, Ian Toyn. An Outline pattern language for Z: five illustrations and two tables. 2003
- full paper
- Susan Stepney, Fiona Polack, Ian Toyn. Patterns to guide practical refactoring: example targetting promotion in Z. 2003
- full paper
- Sandrine Blazy, Frederic Gervais, Regine Laleau. Reuse of specification patterns with the B method. 2003
- Helen Treharne, Steve Schneider, Marchia Bramble. Composing specifications using communication. 2003
- Frederic Peschanski, David Julien. When concurrent control meets functional requirements, or Z + Petri-nets. 2003
- Guilhem Pouzancre. How to design a modern car with a formal B method?. 2003
- Stefan Hallerstede. Parallel hardware design in B. 2003
- Moshe Deutsch, Martin C. Henson, Steve Reeves. Operation refinement and monotonicity in the schema calculus. 2003
- John Derrick, Heike Wehrheim. Using coupled simulations in non-atomic refinement. 2003
- Moshe Deutsch, Martin C. Henson. An Analysis of forward simulation data refinement. 2003
- Jean-Raymond Abrial. B#: Toward a Synthesis between Z and B. 2003
- (invited talk)
- Steve Dunne. Introducing backward refinement into B. 2003
- Bill Stoddart, Frank Zeyda. Expression transformers in B-GSL. 2003
- Annabelle McIver, Carroll Morgan, Thai Son Hoang. Probabilistic termination in B. 2003
- Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan. Probabilistic invariants for probabilistic machines. 2003
- Graeme Smith, Kirsten Winter. Proving temporal properties of Z specifications using abstraction. 2003
- Kirsten Winter, Graeme Smith. Compositional verification for Object-Z. 2003
- John Derrick. Timed CSP and Object-Z. 2003
- Mark Utting, Shaochun Wang. Object orientation without extending Z. 2003
- Nuno Amalio, Fiona Polack. Comparison of formalisation approaches of UML class constructs in Z and object-Z. 2003
- (invited talk)
- Bertrand Meyer. Towards practical proofs of class correctness. 2003
- Robert M. Hierons, Mark Harman, Harbhajan Singh. Automatically generating information from a Z specification to support the classification tree method. 2003
- Christophe Darlot, Jacques Julliand, Olga Kouchnarenko. Refinement preserves PLTL properties. 2003
- Marc Frappier, Regine Laleau. Proving ordering properties for information systems. 2003
- Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, David Currie. ZML: XML support for standard Z. 2003
- Jean-Raymond Abrial, Dominique Cansell, Dominique Mery. Formal derivation of spanning tree algorithms. 2003
- Carla Ferreira, Michael J. Butler. Using B refinement to analyse compensating business processes. 2003
- Christine Poerschke, David E. Lightfoot, John L. Nealon. A Formal specification in B of a medical decision support system. 2003
- Lilian Burdy, Antoine Requet. Extending B with control flow breaks. 2003
- Nazareno Aguirre, Juan C. Bicarregui, Theo Dimitrakos, Thomas S. E. Maibaum. Towards dynamic population management of abstract machines in the B method. 2003
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