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.