Formalizing Convex Hulls Algorithms

David Pichardie 1 Yves Bertot 2
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We study the development of formally proved algorithms for computational geometry. The result of this work is a formal description of the basic principles that make convex hull algorithms work and two programs that implement convex hull computation and have been automatically obtained from formally verified mathematical proofs. A special attention has been given to handling degenerate cases that are often overlooked by conventional algorithm presentations.
Liste complète des métadonnées

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01702679
Contributor : Yves Bertot <>
Submitted on : Wednesday, February 7, 2018 - 9:27:07 AM
Last modification on : Friday, November 16, 2018 - 1:22:05 AM
Document(s) archivé(s) le : Saturday, May 5, 2018 - 3:24:07 AM

File

hulls.pdf
Files produced by the author(s)

Identifiers

Citation

David Pichardie, Yves Bertot. Formalizing Convex Hulls Algorithms. TPHOLs 2001 - 14th International Conference Theorem Proving in Higher Order Logics, Sep 2001, Edinburgh, United Kingdom. pp.346-361, ⟨10.1007/3-540-44755-5_24⟩. ⟨hal-01702679⟩

Share

Metrics

Record views

204

Files downloads

24