Combining Coq and Gappa for Certifying Floating-Point Programs

10 years 11 months ago
Combining Coq and Gappa for Certifying Floating-Point Programs
Abstract. Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floatingpoint 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.
Sylvie Boldo, Jean-Christophe Filliâtre, Gui
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where MKM
Authors Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
Comments (0)