Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Due to a recent revision of Hales's proof of the Kepler Conjecture, the
existing verification of the central graph enumeration procedure had to be
revised because it now has to
cope with more than $10^9$ graphs. This resulted in a new and modular design.
This paper primarily describes the reusable components of the new design:
a while combinator for partial functions, a theory of worklist algorithms, a
stepwise implementation of a data type of sets over a quasi-order
with the help of tries, and a plane graph isomorphism checker. The verification
turned out not to be in vain as it uncovered a bug in Hales's
graph enumeration code.
pdf
BibTeX:
@inproceedings{Nipkow-ITP11,
author={Tobias Nipkow},
title={Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism},
booktitle={Interactive Theorem Proving (ITP 2011)},
editor={van Ekelen and Geuvers and Schmaltz and Wiedijk},
publisher=Springer,series=LNCS,volume={6898},pages={281--296},year=2011}