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

Hi Jens,

-- "Gerlach, Jens" (2017-07-18)
> 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

Interesting to see Alt-Ergo at the top and Z3 at the bottom. That's not usually the case. Do you think you developed these examples (including possibly intermediate assertions) focusing on Alt-Ergo results specifically? This would explain that difference. Also, did you check whether Z3 for some reason gives an error on some of these VCs? That could also explain the drop in performance wrt what we usually see.

> 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.


In our experience, the usefulness of a prover is that it proves something that other provers don't.
With that angle, most provers are very useful.

--
Yannick Moy, Senior Software Engineer, AdaCore



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170718/ca9d5df9/attachment.html>