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
- Subject: [Frama-c-discuss] A problem with math functions
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Mon, 11 Jul 2016 10:36:47 +0200
- In-reply-to: <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F@cea.fr>
- References: <CAA80GKO_sieHDpu3-1E_sTE1TgU0Lw+BwkVNLbia8t0+v_CCsQ@mail.gmail.com> <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F@cea.fr>
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 |
- References:
- [Frama-c-discuss] A problem with math functions
- From: prasuna.drdo at gmail.com (Prasuna Saka)
- [Frama-c-discuss] A problem with math functions
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] A problem with math functions
- Prev by Date: [Frama-c-discuss] A problem with math functions
- Next by Date: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 4
- Previous by thread: [Frama-c-discuss] A problem with math functions
- Next by thread: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 4
- Index(es):