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
_version_ 1783551891859308544
author Rau, Martin
Nipkow, Tobias
author_facet Rau, Martin
Nipkow, Tobias
author_sort Rau, Martin
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324154
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73241542020-06-30 Verification of Closest Pair of Points Algorithms Rau, Martin Nipkow, Tobias Automated Reasoning Article 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. 2020-06-06 /pmc/articles/PMC7324154/ http://dx.doi.org/10.1007/978-3-030-51054-1_20 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Rau, Martin
Nipkow, Tobias
Verification of Closest Pair of Points Algorithms
title Verification of Closest Pair of Points Algorithms
title_full Verification of Closest Pair of Points Algorithms
title_fullStr Verification of Closest Pair of Points Algorithms
title_full_unstemmed Verification of Closest Pair of Points Algorithms
title_short Verification of Closest Pair of Points Algorithms
title_sort verification of closest pair of points algorithms
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324154/
http://dx.doi.org/10.1007/978-3-030-51054-1_20
work_keys_str_mv AT raumartin verificationofclosestpairofpointsalgorithms
AT nipkowtobias verificationofclosestpairofpointsalgorithms

Ejemplares similares