--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on April 2013 ---
Hi, If you look for the proofs of floating-point examples, you can find them on https://www.lri.fr/~sboldo/research.html (I did most of the FP examples of the toccata gallery, but the Coq proofs are only on my web page). On 04/15/2013 05:37 PM, Stephen Siegel wrote: > Claude & Virgile: > Thanks for the pointers. Looking at the examples, it seems that most (but not all) non-trivial verifications of floating-point examples require Coq and therefore some > human intervention (as opposed to being totally automated). Would this be an accurate generalization of the state of the art at this point in time? > I do not fully agree. It mainly depends on what you mean by "non-trivial". If you want clever forward analysis/interval arithmetic, Gappa does that for you (you may have to help it by telling it which variable to bisect), but it works. If you want floating-point tricks, you have to go into interactive proofs. Note that very often, what you need is mathematical proofs, and they have to be done manually. For example, in the cosine example (http://toccata.lri.fr/gallery/MyCosineACSL.en.html), the fact that cos(x) ~ 1-x^2 is the difficult fact that requires Coq. It is not a FP property: everything related to FP is done by gappa here. Hope this helps, Sylvie Boldo > On Apr 15, 2013, at 1:19 AM, Claude March? <Claude.Marche at inria.fr> wrote: > >> >> See >> >> http://toccata.lri.fr/gallery/MyCosineACSL.en.html >> http://hal.inria.fr/hal-00777605 >> >> - Claude >> >> Le 15/04/2013 04:48, Stephen Siegel a ?crit : >>> I'm looking for some simple, interesting floating-point examples that can be proved with Frama-C+Jessie. Here is a good example from the ACSL manual: >>> >>> /*@ requires \abs(\exact(x)) <= 0x1p-5; >>> @ requires \round_error(x) <= 0x1p-20; >>> @ ensures \abs(\exact(\result) - \cos(\exact(x))) <= 0x1p-24; >>> @ ensures \round_error(\result) <= \round_error(x) + 0x3p-24; >>> @*/ >>> float cosine(float x) { >>> return 1.0f - x * x * 0.5f; >>> } >>> >>> However, I can't get any of the theorem provers (CVC3, Z3, Alt-Ergo, Gappa, Simplify) to prove either of the generated VCs. (For all I know, the function may not even satisfy the contract.) Does anyone know of any examples similar to this that can be proved, or have ideas on how to handle this example? >>> Thanks in advance! >>> _______________________________________________ >>> Frama-c-discuss mailing list >>> Frama-c-discuss at lists.gforge.inria.fr >>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >>> >> >> -- >> Claude March? | tel: +33 1 72 92 59 69 >> INRIA Saclay - ?le-de-France | >> Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ >> F-91405 ORSAY Cedex | >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Sylvie Boldo, projet Toccata, Inria Saclay - ?le-de-France PCRI, B?t. 650 - Universit? Paris-Sud - 91405 ORSAY Cedex