TY - GEN
T1 - Verification of Closest Pair of Points Algorithms
AU - Rau, Martin
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - 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 O(nlog n) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.
AB - 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 O(nlog n) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.
UR - http://www.scopus.com/inward/record.url?scp=85088266504&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-51054-1_20
DO - 10.1007/978-3-030-51054-1_20
M3 - Conference contribution
AN - SCOPUS:85088266504
SN - 9783030510534
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 341
EP - 357
BT - Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings
A2 - Peltier, Nicolas
A2 - Sofronie-Stokkermans, Viorica
PB - Springer
T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020
Y2 - 1 July 2020 through 4 July 2020
ER -