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 O(n log n)
of the algorithms. We generate executable code which is empirically
competitive with handwritten reference implementations.
pdf
Spinger web page
BibTeX:
@inproceedings{RauN-IJCAR20,
author={Martin Rau and Tobias Nipkow},
title={Verification of Closest Pair of Points Algorithms},
booktitle={Automated Reasoning (IJCAR 2020)},
editor={N. Peltier and V. Sofronie-Stokkermans},publisher={Springer},
series={LNCS},volume={12167},pages={291--306},year=2020}
Isabelle theories in the
Archive of Formal Proofs