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

Luís Cruz-Filipe; Peter Schneider-Kamp

doi:10.1007/978-3-319-22102-1_10

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

Luís Cruz-Filipe
, Peter Schneider-Kamp

Syddansk Universitet

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › peer 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.

Originalsprog	Engelsk
Tidsskrift	Lecture Notes in Computer Science
Vol/bind	9236
Sider (fra-til)	154-169
Antal sider	16
DOI	https://doi.org/10.1007/978-3-319-22102-1_10
Status	Udgivet - 1 jan. 2015
Udgivet eksternt	Ja
Begivenhed	International Conference on Interactive Theorem Proving - Nanjing, Kina Varighed: 24 aug. 2015 → 27 aug. 2015 Konferencens nummer: 6 https://link.springer.com/book/10.1007/978-3-319-22102-1

Konference

Konference	International Conference on Interactive Theorem Proving
Nummer	6
Land/Område	Kina
By	Nanjing
Periode	24/08/2015 → 27/08/2015
Internetadresse	https://link.springer.com/book/10.1007/978-3-319-22102-1

Adgang til dokumentet

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

Citationsformater

@inproceedings{b9f944f825f4481887165ac3a09e39ff,

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.",

keywords = "Sorting networks, Formal verification, Proof assistants, Certified checker, NP-complete problems",

author = "Lu{\'i}s Cruz-Filipe and Peter Schneider-Kamp",

year = "2015",

month = jan,

day = "1",

doi = "10.1007/978-3-319-22102-1\_10",

language = "English",

volume = "9236",

pages = "154--169",

journal = "Lecture Notes in Computer Science",

note = "International Conference on Interactive Theorem Proving, ITP ; Conference date: 24-08-2015 Through 27-08-2015",

url = "https://link.springer.com/book/10.1007/978-3-319-22102-1",

}

TY - GEN

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

AU - Cruz-Filipe, Luís

AU - Schneider-Kamp, Peter

N1 - Conference code: 6

PY - 2015/1/1

Y1 - 2015/1/1

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.

KW - Sorting networks

KW - Formal verification

KW - Proof assistants

KW - Certified checker

KW - NP-complete problems

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

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

M3 - Conference article

VL - 9236

SP - 154

EP - 169

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - International Conference on Interactive Theorem Proving

Y2 - 24 August 2015 through 27 August 2015

ER -

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

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater