Verification of Closest Pair of Points Algorithms

Martin Rau, Tobias Nipkow

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


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},
Isabelle theories in the Archive of Formal Proofs