Verified efficient enumeration of plane graphs modulo isomorphism

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Scopus citations


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.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - Second International Conference, ITP 2011, Proceedings
Number of pages16
StatePublished - 2011
Event2nd International Conference on Interactive Theorem Proving, ITP 2011 - Berg en Dal, Netherlands
Duration: 22 Aug 201125 Aug 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6898 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference2nd International Conference on Interactive Theorem Proving, ITP 2011
CityBerg en Dal


Dive into the research topics of 'Verified efficient enumeration of plane graphs modulo isomorphism'. Together they form a unique fingerprint.

Cite this