--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2017 ---
Gerlach, Jens wrote: > 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 > Sind die Zahlen nicht priorisiert? Will sagen: hast Du nicht z.B. den CVC3 nur fuer diejenigen Faelle aufgerufen, in denen Alt-Ergo keinen Beweis gefunden hat? Und warum sind die Zahlen so klein? Allein push-heap muesste doch knapp 100 Proof Obligations gehabt haben, und fuer das ganze "ACSL by Example" wuerde ich spontan ca. 1000 erwarten - ? Kann der Qed ca. 900 davon schon alleine loesen? (Hab die Fragen nicht im pdf zu klaeren versucht) Gruss Jochen > 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 > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss