Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"
Software Engineering
2017-01-31 v1 Human-Computer Interaction
Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1701.08470,
title = {Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"},
author = {Lilian Burdy and David Déharbe and Étienne Prun},
journal= {arXiv preprint arXiv:1701.08470},
year = {2017}
}
Comments
In Proceedings F-IDE 2016, arXiv:1701.07925