Skip to Main content Skip to Navigation
Conference papers

Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo 1, 2 Jean-Christophe Filliâtre 1, 2 Guillaume Melquiond 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download
Contributor : Sylvie Boldo <>
Submitted on : Thursday, December 11, 2014 - 11:16:14 AM
Last modification on : Wednesday, September 16, 2020 - 5:09:18 PM
Long-term archiving on: : Thursday, March 12, 2015 - 10:26:48 AM


Files produced by the author(s)




Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩. ⟨inria-00432726⟩



Record views


Files downloads