Formally Proving Size Optimality of Sorting Networks

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind59
Udgave nummer4
Sider (fra-til)425-454
ISSN0168-7433
DOI
StatusUdgivet - 2017

Citer dette

@article{c499aa7fa1524ac29781b62202884c89,
title = "Formally Proving Size Optimality of 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",
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",

}

Formally Proving Size Optimality of Sorting Networks. / Cruz-Filipe, Luis; Larsen, Kim S.; Schneider-Kamp, Peter.

I: Journal of Automated Reasoning, Bind 59, Nr. 4, 2017, s. 425-454.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

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

Y1 - 2017

U2 - 10.1007/s10817-017-9405-9

DO - 10.1007/s10817-017-9405-9

M3 - Journal article

VL - 59

SP - 425

EP - 454

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

ER -