Name
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02614-0_10 | Calculemus/MKM |
Keywords | Field | DocType |
floating-point arithmetic,combining coq,floating-point property,general-purpose logic,coq interactive proof,floating-point program,automatic tool,lack proof automation,lcf approach,certifying floating-point programs,formal verification,interactive theorem,floating point arithmetic,floating point,theorem prover | Theorem provers,Programming language,Floating point,Abstract syntax tree,Automation,Proof obligation,Mathematics,Formal verification,Proof assistant,Speedup | Conference |
Volume | ISSN | Citations |
5625 | 0302-9743 | 26 |
PageRank | References | Authors |
1.12 | 19 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sylvie Boldo | 1 | 292 | 26.85 |
| Jean-Christophe Filliâtre | 2 | 615 | 45.86 |
| Guillaume Melquiond | 3 | 345 | 24.82 |