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 |
| ISSN | 0168-7433 |
| DOIs | |
| Publication status | Published - 2017 |
Bibliographical 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.Keywords
- Interactive theorem proving
- Large-scale proofs
- Program extraction
- Sorting networks