- \n
- Simplified installation with Linux [4.5]<\/li>\n
- Proof Obligation Generation\n
- \n
- For Event-B, specific proof obligations may be generated by the new proof obligation generator: deadlock freeness, non-divergence, feasibility, coverage and exclusivity [4.5]<\/li>\n<\/ul>\n<\/li>\n
- Automatic proof\n
- \n
- \u00a0Interfacing tool \u00ab IAPA \u00bb (Linux only) to connect with provers from Why3\u00a0 platform [4.5]<\/li>\n<\/ul>\n<\/li>\n
- \u00a0Interactive proof\n
- \n
- \u00a0Release of proof drudges, which let user use SMT solvers to define proof rules [4.5]<\/li>\n
- New feature to add its own groups of proof commands [4.5]<\/li>\n
- Improvement in typing of proof commands [4.5]<\/li>\n
- Configurable timeout added to proof commands belonging to pp family [4.4.2]<\/li>\n
- A new proof command added to Apply Tactic [4.4.2]<\/li>\n
- New functionalities in the proof tool to prove rules [4.4.2]<\/li>\n
- Integration of ProB model checker in the interactive prover [4.3]<\/li>\n<\/ul>\n<\/li>\n
- C4B code generator now supports arrays indexed by enumerated type variables [4.5]<\/li>\n
- Editor now displays proof obligations [4.4.2]<\/li>\n
- Coding rules are now verified in the Atelier B [4.3]<\/li>\n<\/ul>\n
New functionalities of the versions 4.4.2 and 4.3 are described in their respective version notes (release notes 4.4.2<\/a> , release note 4.3<\/a> ).<\/p>\n