--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on April 2013 ---
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