| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [17 references]
https://hal.inria.fr/hal-00916880
Contributor : Nicolas Magaud Connect in order to contact the contributor
Submitted on : Tuesday, December 10, 2013 - 8:13:20 PM
Last modification on : Saturday, January 13, 2018 - 1:02:58 AM
Long-term archiving on: : Tuesday, March 11, 2014 - 4:30:11 PM
Contributor : Nicolas Magaud Connect in order to contact the contributor
Submitted on : Tuesday, December 10, 2013 - 8:13:20 PM
Last modification on : Saturday, January 13, 2018 - 1:02:58 AM
Long-term archiving on: : Tuesday, March 11, 2014 - 4:30:11 PM
File
CH-submitted2011.pdf
Publisher files allowed on an open archive