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.

• Type: Conference
• Year: 2009
• Where: MKM
• Authors: Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
• Keywords: Coq Interactive Proof, Information Management, Interactive Theorem Provers, MKM 2009, Restrictive Logics