Formally Proving Size Optimality of Sorting Networks

Luis Cruz-Filipe; Kim S. Larsen; Peter Schneider-Kamp

doi:10.1007/s10817-017-9405-9

Formally Proving Size Optimality of Sorting Networks

Luis Cruz-Filipe
, Kim S. Larsen
, Peter Schneider-Kamp

University of Southern Denmark

Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review

Abstract

Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.

Original language	English
Journal	Journal of Automated Reasoning
Volume	59
Issue number	4
Pages (from-to)	425-454
Number of pages	30
ISSN	0168-7433
DOIs	https://doi.org/10.1007/s10817-017-9405-9
Publication status	Published - 1 Feb 2017
Externally published	Yes

Keywords

Interactive theorem proving
Large-scale proofs
Program extraction
Sorting networks

Access to Document

10.1007/s10817-017-9405-9

Cite this

@article{73e205c1c2394123a294eb29d445ed88,

title = "Formally Proving Size Optimality of Sorting Networks",

abstract = "Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.",

keywords = "Interactive theorem proving, Large-scale proofs, Program extraction, Sorting networks",

author = "Luis Cruz-Filipe and Larsen, \{Kim S.\} and Peter Schneider-Kamp",

note = "Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.",

year = "2017",

month = feb,

day = "1",

doi = "10.1007/s10817-017-9405-9",

language = "English",

volume = "59",

pages = "425--454",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer",

number = "4",

}

TY - JOUR

T1 - Formally Proving Size Optimality of Sorting Networks

AU - Cruz-Filipe, Luis

AU - Larsen, Kim S.

AU - Schneider-Kamp, Peter

N1 - Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.

PY - 2017/2/1

Y1 - 2017/2/1

N2 - Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.

AB - Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time. In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.

KW - Interactive theorem proving

KW - Large-scale proofs

KW - Program extraction

KW - Sorting networks

U2 - 10.1007/s10817-017-9405-9

DO - 10.1007/s10817-017-9405-9

M3 - Journal article

SN - 0168-7433

VL - 59

SP - 425

EP - 454

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 4

ER -

Formally Proving Size Optimality of Sorting Networks

Abstract

Keywords

Access to Document

Fingerprint

Cite this