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] A problem with math functions


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                    |