Version 4.5 of Atelier B

Atelier B 4.5.0 is a Community Edition version, freely downloadable

This version fixes, cumulatively  since version 4.2.1, 146 bugs and several improvements are included:

• Simplified installation with Linux
• Proof Obligation Generation
  • For Event-B, specific proof obligations may be generated by the new proof obligation generator: deadlock freeness, non-divergence, feasibility, coverage and exclusivity
• Automatic proof
  •  Interfacing tool « IAPA » (Linux only) to connect with provers from Why3  platform
•  Interactive proof
  •  Release of proof drudges, which let user use SMT solvers to defines proof rules
  • New feature to add its own groups of proof commands
  • Improvement in typing of proof commands
  • Configurable timeout added to proof commands belonging to pp family
  • A new proof command added to Apply Tactic
  • New functionalities in the proof tool to prove rules
  • Integration of ProB model checker in the interactive prover
• C4B code generator now supports arrays indexed by enumerated type variables
• Editor now displays proof obligations
• Coding rules are now verified in the Atelier B

New functionalities of the versions 4.4.2 and 4.3 are described in their respective version notes (release notes 4.4.2 , release note 4.3 ).

If you require more detailed information please refer to the 4.5 release notes