Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] ACSL by Example and automatic provers
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Tue, 18 Jul 2017 09:53:20 +0000
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