Combining coq and gappa for certifying floating-point programs

Sylvie Boldo; Jean Christophe Filliâtre; Guillaume Melquiond

doi:10.1007/978-3-642-02614-0_10

Combining coq and gappa for certifying floating-point programs

Sylvie Boldo, Jean Christophe Filliâtre, Guillaume Melquiond

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings
Pages	59-74
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-02614-0_10
Publication status	Published - 28 Aug 2009
Externally published	Yes
Event	16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 - Grand Bend, ON, Canada Duration: 6 Jul 2009 → 12 Jul 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5625 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009
Country/Territory	Canada
City	Grand Bend, ON
Period	6/07/09 → 12/07/09

Access to Document

10.1007/978-3-642-02614-0_10

Cite this

Boldo, S., Filliâtre, J. C., & Melquiond, G. (2009). Combining coq and gappa for certifying floating-point programs. In Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings (pp. 59-74). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5625 LNAI). https://doi.org/10.1007/978-3-642-02614-0_10

Boldo, Sylvie ; Filliâtre, Jean Christophe ; Melquiond, Guillaume. / Combining coq and gappa for certifying floating-point programs. Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. 2009. pp. 59-74 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9ecfef5699494f179e776a6525c6824f,

title = "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 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.",

author = "Sylvie Boldo and Filli{\^a}tre, \{Jean Christophe\} and Guillaume Melquiond",

year = "2009",

month = aug,

day = "28",

doi = "10.1007/978-3-642-02614-0\_10",

language = "English",

isbn = "3642026133",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "59--74",

booktitle = "Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings",

note = "16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 ; Conference date: 06-07-2009 Through 12-07-2009",

}

Boldo, S, Filliâtre, JC & Melquiond, G 2009, Combining coq and gappa for certifying floating-point programs. in Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5625 LNAI, pp. 59-74, 16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009, Grand Bend, ON, Canada, 6/07/09. https://doi.org/10.1007/978-3-642-02614-0_10

Combining coq and gappa for certifying floating-point programs. / Boldo, Sylvie; Filliâtre, Jean Christophe; Melquiond, Guillaume.
Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. 2009. p. 59-74 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5625 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Combining coq and gappa for certifying floating-point programs

AU - Boldo, Sylvie

AU - Filliâtre, Jean Christophe

AU - Melquiond, Guillaume

PY - 2009/8/28

Y1 - 2009/8/28

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-02614-0_10

DO - 10.1007/978-3-642-02614-0_10

M3 - Conference contribution

AN - SCOPUS:69149095551

SN - 3642026133

SN - 9783642026133

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 59

EP - 74

BT - Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings

T2 - 16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009

Y2 - 6 July 2009 through 12 July 2009

ER -

Boldo S, Filliâtre JC, Melquiond G. Combining coq and gappa for certifying floating-point programs. In Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings. 2009. p. 59-74. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02614-0_10

Combining coq and gappa for certifying floating-point programs

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this