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

Lilian Burdy, David Déharbe, Étienne Prun

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 At…