Verification of Closest Pair of Points Algorithms

We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of [Formula: see text] of the alg...

Descripción completa

Detalles Bibliográficos
Autores principales: Rau, Martin, Nipkow, Tobias
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324154/
http://dx.doi.org/10.1007/978-3-030-51054-1_20
Descripción
Sumario:We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of [Formula: see text] of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.

Ejemplares similares