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. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Boldo, S., Filliâtre, J. C., & Melquiond, G. (2009). Combining coq and gappa for certifying floating-point programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5625 LNAI, pp. 59–74). https://doi.org/10.1007/978-3-642-02614-0_10
Mendeley helps you to discover research relevant for your work.