Top

Published in:

2015 | OriginalPaper | Chapter

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

Authors : Luís Cruz-Filipe, Peter Schneider-Kamp

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

next chapter Proof-Producing Reflection for HOL

The logs and the Java verifier are available at http://imada.sdu.dk/~petersk/sn/.

Comparator (i, j) in comparator network \(C;(i,j);C'\) is redundant if \({\varvec{x}}_i<{\varvec{x}}_j\) for all \({\varvec{x}}\in \mathsf {outputs}(C)\) – in other words, (i, j) never changes its inputs.

Appel, K., Haken, W.: Every planar map is four colorable. Part I: discharging. Ill. J. Math. 21, 429–490 (1977)MATHMathSciNet

Appel, K., Haken, W., Koch, J.: Every planar map is four colorable. Part II: reducibility. Ill. J. Math. 21, 491–567 (1977)MATHMathSciNet

Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Trans. A Roy. Soc. 363(1835), 2351–2375 (2005)MATHMathSciNetCrossRef

Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): ITP 2013. LNCS, vol. 7998. Springer, Heidelberg (2013) MATH

Claret, G., González-Huesca, L.C., Régis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In Blazy et al. [4], pp. 67–83

Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186–193. IEEE (2014)

Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schauß, M., (ed.) RTA 2011. LIPIcs, vol. 10, pp. 21–30. Schloss Dagstuhl (2011)

Cruz-Filipe, L., Schneider-Kamp, P.: Optimizing a certified proof checker for a large-scale computer-generated proof. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 55–70. Springer, Heidelberg (2015) CrossRef

Floyd, R.W., Knuth, D.E.: The Bose-Nelson sorting problem. In: Srivastava, J.N. (ed.) A Survey of Combinatorial Theory, pp. 163–172. North-Holland, Amsterdam (1973)

10.

Fouilhe, A., Monniaux, D., Périn, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 345–365. Springer, Heidelberg (2013) CrossRef

11.

Gonthier, G.: Formal proof - the four-color theorem. Not. AMS 55(11), 1382–1393 (2008)MATHMathSciNet

12.

Knuth, D.E.: The Art of Computer Programming. Sorting and Searching, vol. 3. Addison-Wesley, Reading (1973)

13.

Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219–226. Springer, Heidelberg (2014)

14.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

15.

Parberry, I.: A computer-assisted optimal depth lower bound for nine-input sorting networks. Math. Syst. Theor. 24(2), 101–116 (1991)MATHMathSciNetCrossRef

16.

Sternagel, C., Thiemann, R.: The certification problem format. In: Benzmüller, C., Paleo, B.W. (eds.) UITP 2014. EPTCS, vol. 167, pp. 61–72 (2014)

17.

Thiemann, R.: Formalizing bounded increase. In: Blazy et al. [4], pp. 245–260

18.

van Voorhis, D.C.: Toward a lower bound for sorting networks. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 119–129. Plenum Press, New York (1972)CrossRef

Title: Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Authors: Luís Cruz-Filipe
Peter Schneider-Kamp
Publisher: Springer International Publishing
Book: Interactive Theorem Proving
Print ISBN: 978-3-319-22101-4

Electronic ISBN: 978-3-319-22102-1

Copyright Year: 2015
DOI: https://doi.org/10.1007/978-3-319-22102-1_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner