--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2017 ---
Hello, Frama-C/WP and Why3 allows using several automatic theorem provers to discharge verification conditions. For âACSL by Exampleâ (https://fraunhoferfokus.github.io/acsl-by-example/) we employ Alt-Ergo, Z3, CVC4, CVC3, and Eprover. Of course, we pass only those conditions to the provers that havenât been discharged already by WPâs built-in simplifier Qed. In case you want to know how these provers succeed on our examples, we provide here a short summary of the results presented in Appendix A.3 (Pages 183) of https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf Of the 59 examples whose proof obligations could automatically discharged 55 can be completely verified by just using Alt-Ergo 51 can be completely verified by just using CVC3 47 can be completely verified by just using CVC4 26 can be completely verified by just using Eprover 9 can be completely verified by just using Z3 This is of course a very rough statistics and I would like to emphasize that due to the limited number of our examples this ordering does not reflect on the usefulness of the individual provers. Regards Jens