Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"

Lilian Burdy
(Clearsy System Engineering)
David Déharbe
(Clearsy System Engineering)
Étienne Prun
(Clearsy System Engineering)

The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically. Consequently, such proof obligations are often cluttered with information that is irrelevant to establish their validity.

We present iapa, an "Interface to Automatic Proof Agents", a new tool that is being integrated to Atelier~B, through which the user will access proof obligations, apply operations to simplify these proof obligations, and then dispatch the resulting, simplified, proof obligations to a portfolio of automatic theorem provers.

In Catherine Dubois, Paolo Masci and Dominique Méry: Proceedings of the Third Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016, Electronic Proceedings in Theoretical Computer Science 240, pp. 82–90.
Published: 27th January 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: