* Formal Methods * Z notation * B User Group

The B-Method

Please mail J.P.Bowen@reading.ac.uk if you know of relevant on-line information not included here or would like to maintain information on a particular topic.

* B'98: 2nd International B Conference, Montpellier, France, 22-24 April 1998.
See photographs.

This document contains some pointers to information relating to the B-Method, and its associated tool support, available around the world on the World Wide Web (WWW or W3), a global hypermedia system providing worldwide information.


The B-Method has been developed by Jean-Raymond Abrial - also originator of the Z notation - and others. B is a formal method for the development of program code from a specification in the Abstract Machine Notation. It includes tool support and has been used in some significant industrial applications (e.g., by GEC Alsthom).

On-line resources

B User Group (BUG).
See also BUG phone book and FTP site.

Email listserv@estas1.inrets.fr with the message "subscribe bug" to join the BUG mailing list. Contact Georges Mariano on mariano@terre.inrets.fr for further BUG information.

Atelier-B, France.
B software development environment. See the boiler case study.

Information also available in French. See La Lettre B newsletter.

B-Core (UK) Limited, UK.
Markets the B-Toolkit.

Email Ib.Sorensen@comlab.ox.ac.uk for further information.

Teesside B-Resource.
Provides much on-line information concerning B, including information on the various B-Technologies

A mailing list for discussion about B has been established. Send an email message containing "subscribe b-talk" to b-talk-request@tees.ac.uk to join.



See the definitive * B bibliography. A searchable version is also available as part of the excellent Collection of Computer Science Bibliographies.

A list of references relevant to B is available on-line from the Z bibliography.

Both bibliographies are in BibTeX format suitable for use with the LaTeX document preparation system.


The following definitive book on B is available: See also: ! B books listed by Amazon.

Tool support

The B-Tool is a language interpreter and a run-time environment for supporting B. The B-Toolkit is a set of integrated tools which fully supports the B-Method for formal software development, built on top of the B-Tool. These tools are available from B-Core (UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA, UK. For further details, contact Ib Sørensen on Ib.Sorensen@comlab.ox.ac.uk (tel +44-1865-784520, fax +44-1865-784518).

Atelier B, a tool supporting the Abstract Machine Notation (AMN), is available under licence. from Digilog, France. Features include syntax, type and static semantics checking, proof support, refinement, a graphical interface and pretty-printing. An animator is planned. Test case generation is not supported. Contact Francois Bustany on digilog@dialup.francenet.fr (tel: +33 42 39 93 19, fax: +33 42 24 38 06).

Further information: Atelier B is composed of a complete set of integrated tools enabling the development of applications using the method invented by Jean-Raymond Abrial, the B-Method. Atelier B assists developers in the formalization of their aplications, performing automatically on specifications and their refinements, syntax analysis, type checking, generation and demonstration of proof obligations. Extra components are supplied such as translators into current computer programming languages (C, Ada, ...), a mathematical editor, libraries of predefined machines and various project analysis tools. Access to Atelier B software tools is by a graphical MOTIF interface or by a batch language; in each mode it manages multi-users projects. Atelier B has been designed by Digilog and GEC Alsthom Transport in close collaboration with Jean-Raymond Abrial. The first version of Atelier B will be upgraded in 1995 with an animator of specifications, a new generation of prover, a powerful project documentation generator and various interfaces with standard tools (SGML, Interleaf, ...). Atelier B is sponsored by RATP, SNCF and INRETS and developed with their technical co-operation.

See also:


The collaborative B User Trials (BUT) project and the MaFMeth Project (also supporting VDM-SL) at RAL and elsewhere in the UK, are investigating the use of B.


The International B Conference Steering Committee (Association de Pilotage des Conférences B - APCB) organizes the International B Conference:
  1. 1st B Conference, Nantes, France, 25-27 November 1996. See photographs.

  2. B'98: 2nd International B Conference, Montpellier, France, 22-24 April 1998. See photographs.

  3. ! FM'99: B-Method mini-track and User Group Meeting, Toulouse, France, 20-24 September 1999.

  4. ! BZ2000: International Conference of B and Z Users, York, UK, 28 August - 2 September 2000.

    See also:
    Last updated by Jonathan Bowen, 25 March 1999.
    Further information for possible inclusion is welcome.

    Part of the OUCL archive.