--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example and automatic provers



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