--- layout: fc_discuss_archives title: Message 7 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



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