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

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

Abstract

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
PublisherSpringer
Publication date2015
Pages154-169
ISBN (Print)978-3-319-22101-4
ISBN (Electronic)978-3-319-22102-1
DOIs
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science
Volume9236
ISSN0302-9743

Fingerprint

Sorting
Computer science
Color

Cite this

Cruz-Filipe, L., & Schneider-Kamp, P. (2015). Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. In C. Urban, & X. Zhang (Eds.), Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (pp. 154-169). Springer. Lecture Notes in Computer Science, Vol.. 9236 https://doi.org/10.1007/978-3-319-22102-1_10
Cruz-Filipe, Luís ; Schneider-Kamp, Peter. / Formalizing Size-Optimal Sorting Networks : Extracting a Certified Proof Checker. Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. editor / Christian Urban ; Xingyuan Zhang. Springer, 2015. pp. 154-169 (Lecture Notes in Computer Science, Vol. 9236).
@inproceedings{b9ad4e1742604501b4fc7e868c2babb1,
title = "Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker",
abstract = "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.",
author = "Lu{\'i}s Cruz-Filipe and Peter Schneider-Kamp",
year = "2015",
doi = "10.1007/978-3-319-22102-1_10",
language = "English",
isbn = "978-3-319-22101-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "154--169",
editor = "Christian Urban and Xingyuan Zhang",
booktitle = "Interactive Theorem Proving",
address = "Germany",

}

Cruz-Filipe, L & Schneider-Kamp, P 2015, Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. in C Urban & X Zhang (eds), Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. Springer, Lecture Notes in Computer Science, vol. 9236, pp. 154-169. https://doi.org/10.1007/978-3-319-22102-1_10

Formalizing Size-Optimal Sorting Networks : Extracting a Certified Proof Checker. / Cruz-Filipe, Luís; Schneider-Kamp, Peter.

Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. ed. / Christian Urban; Xingyuan Zhang. Springer, 2015. p. 154-169 (Lecture Notes in Computer Science, Vol. 9236).

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

TY - GEN

T1 - Formalizing Size-Optimal Sorting Networks

T2 - Extracting a Certified Proof Checker

AU - Cruz-Filipe, Luís

AU - Schneider-Kamp, Peter

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-22102-1_10

DO - 10.1007/978-3-319-22102-1_10

M3 - Article in proceedings

SN - 978-3-319-22101-4

T3 - Lecture Notes in Computer Science

SP - 154

EP - 169

BT - Interactive Theorem Proving

A2 - Urban, Christian

A2 - Zhang, Xingyuan

PB - Springer

ER -

Cruz-Filipe L, Schneider-Kamp P. Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker. In Urban C, Zhang X, editors, Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. Springer. 2015. p. 154-169. (Lecture Notes in Computer Science, Vol. 9236). https://doi.org/10.1007/978-3-319-22102-1_10