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: jochen.burghardt at fokus.fraunhofer.de (jochen.burghardt at fokus.fraunhofer.de)
• Date: Tue, 18 Jul 2017 14:07:00 +0200
• In-reply-to: <F3DA813E-423C-4D8C-997A-92FC1E00F0F1@fokus.fraunhofer.de>
• References: <F3DA813E-423C-4D8C-997A-92FC1E00F0F1@fokus.fraunhofer.de>

---

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

---

• References:
  • [Frama-c-discuss] ACSL by Example and automatic provers
    • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)

• Prev by Date: [Frama-c-discuss] ACSL by Example and automatic provers
• Next by Date: [Frama-c-discuss] ACSL by Example and automatic provers
• Previous by thread: [Frama-c-discuss] ACSL by Example and automatic provers
• Next by thread: [Frama-c-discuss] ACSL by Example and automatic provers
• Index(es):
  • Date
  • Thread