Verified efficient enumeration of plane graphs modulo isomorphism

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

6 Scopus citations

Abstract

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
Pages281-296
Number of pages16
DOIs
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

Conference

Conference2nd International Conference on Interactive Theorem Proving, ITP 2011
Country/TerritoryNetherlands
CityBerg en Dal
Period22/08/1125/08/11

Fingerprint

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

Cite this