Atelier B

Atelier B is a tool enabling the operational use of B method. In a coherent environment, it provides many functions for managing projects in B language.


These functions can be divided into four categories:

  • proof aid, to demonstrate proof obligations using suitable proof tools
  • Development aid: automatic management of dependency between B components,
  • User comfort tools: graphical representation of projects, display of project status and statistics, project archiving.

Use of Atelier B

Atelier B is either used via a Man Machine Interface in QT format or using the commands directly (command mode). Atelier B is multi-user. Tasks that can be automated during project development are the following:

  • Syntax verification of components
  • Automatic proof obligation generation
  • Automatic translation of B installations to C or Ada language

Currently, Atelier B is available in Windows, Linux, Mac OS and Solaris operating systems.

ATELIER B 4.7 and website

Download the main 4.7’s features.

visit the web site:

Need a custom-made system ?

We are safety software and systems designers.  Contact us and let's discuss your project together!