Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls

Abstract : This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.
Type de document :
Communication dans un congrès
Jacques Fleuriot & Testsuo Ida. Automated Deduction in Geometry (Post-proceedings), Sep 2012, Edinbourg, United Kingdom. Springer, pp.71-88, 2012, LNCS. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-40672-0_6#page-1〉. 〈10.1007/978-3-642-40672-0_6〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00916880
Contributeur : Nicolas Magaud <>
Soumis le : mardi 10 décembre 2013 - 20:13:20
Dernière modification le : samedi 13 janvier 2018 - 01:02:58
Document(s) archivé(s) le : mardi 11 mars 2014 - 16:30:11

Fichier

CH-submitted2011.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Christophe Brun, Jean-François Dufourd, Nicolas Magaud. Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls. Jacques Fleuriot & Testsuo Ida. Automated Deduction in Geometry (Post-proceedings), Sep 2012, Edinbourg, United Kingdom. Springer, pp.71-88, 2012, LNCS. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-40672-0_6#page-1〉. 〈10.1007/978-3-642-40672-0_6〉. 〈hal-00916880〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

338