Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs.

In this paper, we describe a formalized theory of size-optimal sorting networks. From this formalization we extract a certified checker that successfully verifies computer-generated proofs of optimality on up to 8 inputs. The checker relies on an untrusted oracle to shortcut the search for witnesses on more than 1.6 million NP-complete subproblems.
Original languageEnglish
Title of host publicationInteractive Theorem Proving : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
EditorsChristian Urban, Xingyuan Zhang
Publication date2015
ISBN (Print)978-3-319-22101-4
ISBN (Electronic)978-3-319-22102-1
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker'. Together they form a unique fingerprint.

Cite this