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

INRIA
INRIA Saclay, Laboratoire de Recherche en Informatique (LRI), Université Paris Sud

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings
Pages	59-74
Nombre de pages	16
Les DOIs	https://doi.org/10.1007/978-3-642-02614-0_10
état	Publié - 28 août 2009
Modification externe	Oui
Evénement	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 Durée: 6 juil. 2009 → 12 juil. 2009

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5625 LNAI
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	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
Pays/Territoire	Canada
La ville	Grand Bend, ON
période	6/07/09 → 12/07/09

Accès au document

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

Contient cette citation

Boldo, S., Filliâtre, J. C., & Melquiond, G. (2009). Combining coq and gappa for certifying floating-point programs. Dans Intelligent Computer Mathematics - 16th Symposium, Calculemus 2009 - 8th International Conference, MKM 2009 - Held as Part of CICM 2009, Proceedings (p. 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. p. 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. Dans 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, p. 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation