- Formally Proving Size Optimality of Sorting Networks.
- Luís Cruz-Filipe, Kim S. Larsen, and Peter Schneider-Kamp.
Journal of Automated Reasoning. Accepted for Publication.
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.
- Link to the publication at the publisher's site - subscription may be required.
Text required by the publisher (if any):
The final publication is available at link.springer.com.
open access (563 KB)
The same as the publisher's version, when the publisher permits. Otherwise, the author's last version before the publisher's copyright; this is often exactly the same, but sometimes fonts, page numbers, figure numbers, etc. are different. It may also be a full version. However, it is safe to read this version, and at the same time cite the official version, as long as references to concrete locations, numbered theorems, etc. inside the article are avoided.
Other publications by the author.