Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Yves Bertot Connect in order to contact the contributor
Submitted on : Wednesday, February 7, 2018 - 9:27:07 AM
Last modification on : Thursday, January 20, 2022 - 4:18:36 PM
Long-term archiving on: : Saturday, May 5, 2018 - 3:24:07 AM


Files produced by the author(s)



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⟩



Les métriques sont temporairement indisponibles