Download Atelier B

 Atelier B Support & Maintenance


The Atelier B V4 is distributed free of charge, through its Community Version, to all those who wish to use Atelier B for research, teaching and development of their industrial projects. As soon as the tool is used for the first time it is allocated for an unlimited time.

The atelier B V4 comprises all the tools required for developing an industrial project and is available in WINDOWS, MAC and LINUX.

Users, companies and research or teaching organisations can subscribe to a maintenance contract for the latest version (corrective or with new functional features). The licence contract supplied with Atelier B can be obtained upon request, in French and English, at atelierb (at) clearsy (dot) com .





  • Atelier B CSSP: B modelling and application programming for CLEARSY Safety Platform starter kit SK0
  • Atelier B now supports macOS 10.15 « Catalina »
  • Interactive proof
    • Saved proofs can now be replayed until the first failing command
    • User pass can now be saved in the patchprover file
  • Project management
    • Improvement of the use of MANIFEST
    • MANIFEST files can now be used through the console
  • Translator
    • C4B: add the translation of tables indexed by an enumeration.
    • B2C: control on table initialization
  • Proof drudge
    • Use of real numbers
    • It is now possible to add only rule validated by PP
  • NPOG
    • Event-B: add the WITNESS keyword
    • Consolidation of PO generation
  • Addition of the proof obligation generator parametrization manual


  • Simplified installation with Linux (Universal Installer)
  • For Event-B, specific proof obligations may be generated by the new proof obligation generator: deadlock freeness, non-divergence, feasibility, coverage and exclusivity
  • Interfacing tool « IAPA » (Linux only) to connect with provers from Why3 platform
  • Interactive proof
    • New feature to use SMT solvers to define proof rules applying to the current goal
    • New feature to add its own groups of proof commands
    • Improvement in typing of proof commands
    • C4B code generator now supports arrays indexed by enumerated type variables


  • Proof obligations displayed in the model editor.
  • A new proof command at for Apply Tactic.
  • A configurable timeout for the pp family proof commands.
  • New functionalities for the Proof Rules Validator.


  • Checking of coding rules inside B models.
  • Integration of ProB model-checker inside the interactive prover interface


  • Full 64-bit support
  • A new traceable, generic, proof obligation generator
  • A better integration of real and floating point numbers
  • Accessors added to BART in order to solve refinement conflicts
  • Boolean and integer translation fine-tuning in C4B code generator
  • Addition of a proof server, in order to speed up proof


  • Improved support of integers : maximum implementable value (MAXINT) can be 16, 32 or 64 bit-wide, integer literals are not bounded (BigINT)
  • Experimental support of real numbers
  • Experimental support of floating point numbers
  • Support of hexadecimal literals.
  • New C code generator, C4B, with translation profile and makefile creation.
  • Localization of the software in English, French, Japanese, and Portuguese.
  • Support of Unicode. Strings and comments may contain non-ASCII characters.
  • Addition of a components status graphical view
  • Parallel execution of proof tasks
  • Improved Integrated Editor
  • The interactive prover displays pending goals
  • Generation of coverage and exclusivity proof obligations
  • Tool for validating user added mathematical rules
  • Spell-checking B model comments
  • Mathematical rules displayed in the view “Theory List” are sorted according to their applicability
  • B model editor informs the user when the edited file has been modified on the disk.
  • Addition of a search function “à la grep”
  • Added rules when using the command “pc” are now displayed.

More informations about "Atelier B Support & Maintenance"

Copy link
Powered by Social Snap