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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 109, Issue 4



Hello Loïc,

>   Just to mention it, the appendix A.3 of this document shows the individual results of _each_ provers and for each algorithm.
>    It is interesting to observe that, in most cases, Alt-Ergo, CVC4, CVC4, and Z3 have very *closed* results, and Eprover is significantly aside.
 >   In the table provided by Jens, most provers (except Eprover) completely verify all the verification conditions but a few.

Your observation is right.
Eprover looks better than Z3 in my statistics because it works very well on the many small “stack*” examples.
On the more complex examples, Eprover is not particular good, except (interestingly) on the numeric algorithms.
    
 >   A possible next step would be to extract the « difficult » verification conditions and understand what is going wrong with them for each prover.

Let’s looks for a project!-)
    
>    Second remark, regarding WP, it would be interesting to compare the results obtained with its native support of Alt-Ergo, or via 
>    the Why-3 translation.
>    Namely, comparing -wp-prover alt-ergo and -wp-prover why3:alt-ergo in order to understand the impact of Why-3 translation.
 
The Alt-Ergo data in Appendix A.3 were obtained using Why3.
The Alt-Ergo data in Appendix A.2 were obtained using -wp-prover alt-ergo.

Jens