TY - GEN
T1 - Verified efficient enumeration of plane graphs modulo isomorphism
AU - Nipkow, Tobias
PY - 2011
Y1 - 2011
N2 - 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 109 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.
AB - 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 109 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.
UR - http://www.scopus.com/inward/record.url?scp=80052137463&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22863-6_21
DO - 10.1007/978-3-642-22863-6_21
M3 - Conference contribution
AN - SCOPUS:80052137463
SN - 9783642228629
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 281
EP - 296
BT - Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings
T2 - 2nd International Conference on Interactive Theorem Proving, ITP 2011
Y2 - 22 August 2011 through 25 August 2011
ER -