Atelier B proof obligation generator was developped in the early 90’s. Developped with the prolog-like “theory language”, this tool is very sensible to modifications and difficult to adapt to language extensions/modifications. The idea is to develop a generic proof obligation generator that can:
- support both B and event-B proof obligations
- be easily modifiable/extandable, to generate specific proof obligations.
Developments started in 2011, within the framework of the CERCLES-2 R&D project.
Is there any date for the availability of the tool ? its specification ?
The project started late because of administrative problems.
A prototype is expected by the end of the year, released on sourceforge as usual.