--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on July 2016 ---
Le 11/07/2016 09:30, Loïc Correnson a écrit : > One reason is that many SMT solvers (if not all) lack interesting properties about trigonometry. Yes, as far as I know, no SMT solver know about trigonometry. But there are other provers available as Why3 back-end that do, and Why3 drivers indeed know how to use them : MetiTarski, Coq, Isabelle/HOL For proving floating-point programs correct w.r.t a specification involving real numbers, it is mandatory to use provers outside the SMT world. See for examples http://toccata.lri.fr/gallery/fp.en.html - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |