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] floating-point examples

Hello,

2013/4/15 Stephen Siegel <siegel at udel.edu>:
> 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?

You have examples of verification of floating-point computations on
Toccata's gallery of verified programs
(http://toccata.lri.fr/gallery/fp.en.html). Your specific cosine
example looks like my_cos3 in this example:
http://toccata.lri.fr/gallery/MyCosineACSL.en.html, where the
description states that not all proof obligations are discharged
automatically and some Coq is needed.

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile