Development of a generic proof obligation generator

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.

Ce contenu a été publié dans Research, Tools. Vous pouvez le mettre en favoris avec ce permalien.

2 réponses à Development of a generic proof obligation generator

  1. interested dit :

    Is there any date for the availability of the tool ? its specification ?

  2. ClearSy dit :

    The project started late because of administrative problems.
    A prototype is expected by the end of the year, released on sourceforge as usual.

Laisser un commentaire