Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Formally Proving Size Optimality of Sorting Networks

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. Numbering from 0, rather than from 1, simplifies some aspects of the formalization.

  2. This intuition is made precise by the program extraction mechanism of Coq [30], which generates precisely this algorithm.

  3. The indirect way in which this is done is unfortunately typical of program extraction, and adds some layers of complexity to what a direct program would achieve.

  4. Technically, we are formalizing just the oracle data: the result of the oracle (a computer program), rather than the program itself (which we do not want to formalize). We deliberately blur the distinction between these concepts in this section.

References

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

    MATH  Google Scholar 

  2. Appel, K., Haken, W.: The four color proof suffices. Math. Intell. 8(1), 10–20 (1986)

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  4. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science. Springer, Berlin (2004)

    Book  MATH  Google Scholar 

  5. Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21, 827–859 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  6. Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving, ITP 2013, Proceedings, LNCS, vol. 7998. Springer, Berlin (2013)

  7. Bundala, D., Závodný, J.: Optimal sorting networks. In: A.H. Dediu, C. Martín-Vide, J.L. Sierra-Rodríguez, B. Truthe (eds.) LATA, LNCS, vol. 8370, pp. 236–247. Springer, Berlin (2014)

  8. Chung, M.J., Ravikumar, B.: Bounds on the size of test sets for sorting and related networks. Discrete Math. 81(1), 1–9 (1990)

    Article  MATH  MathSciNet  Google Scholar 

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

  10. 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)

  11. Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Sorting nine inputs requires twenty-five comparisons. J. Comput. Syst. Sci. 82(3), 551–563 (2016)

    Article  MATH  MathSciNet  Google Scholar 

  12. 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). http://www.dagstuhl.de/dagpub/978-3-939897-30-9

  13. Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electron. Notes Comput. Sci. 151(1), 75–91 (2006)

    Article  MATH  Google Scholar 

  14. Cruz-Filipe, L., Schneider-Kamp, P.: Formalizing size-optimal sorting networks: extracting a certified proof checker. In: C. Urban, X. Zhang (eds.) ITP 2015, LNCS, vol. 9236, pp. 154–169. Springer, Berlin (2015)

  15. 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, LNAI, vol. 9150, pp. 55–70. Springer (2015)

  16. Cruz-Filipe, L., Wiedijk, F.: Hierarchical reflection. In: Slind, K., Bunker, A., Gopalakrishnan,G. (eds.) TPHOLs, LNCS, vol. 3223, pp. 66–81. Springer, Berlin (2004)

  17. Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: ICTAC, Lecture Notes in Computer Science, vol. 6255, pp. 260–274. Springer, Berlin (2010)

  18. Erkök, L., Matthews, J.: Using Yices as an automated solver in Isabelle/HOL. In: Automated Formal Methods’08, pp. 3–13. ACM Press, Princeton, NJ, USA (2008)

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

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

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

    MATH  MathSciNet  Google Scholar 

  22. Harrison, J.: HOL Light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD, Lecture Notes in Computer Science, vol. 1166, pp. 265–269. Springer, Berlin (1996)

  23. Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and maple. J. Autom. Reason. 21(3), 279–294 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  24. Heule, M., Kullmann, O., Marek, V.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016, Lecture Notes in Computer Science, vol. 9710, pp. 228–245. Springer, Berlin (2016)

  25. Johnson, D.S.: The np-completeness column: an ongoing guide. J. Algorithms 3, 288–300 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  26. Knuth, D.: The Art of Computer Programming, Volume III: Sorting and Searching. Springer, Reading (1973)

    MATH  Google Scholar 

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

  28. Krebbers, R., Spitters, B.: Computer certified efficient exact reals in Coq. In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Calculemus 2011, LNCS, vol. 6824, pp. 90–106. Springer, Berlin (2011)

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

    Article  Google Scholar 

  30. Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008, LNCS, vol. 5028, pp. 359–369. Springer, Berlin (2008)

  31. McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES, LNCS, vol. 2277, pp. 197–216. Springer, Berlin (2002)

  32. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)

    MATH  Google Scholar 

  33. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007)

  34. O’Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008, LNCS, vol. 5170, pp. 246–261. Springer, Berlin (2008)

  35. Oury, N.: Observational equivalence and program extraction in the Coq proof assistant. In: Hofmann, M. (ed.) TLCA 2003, LNCS, vol. 2701, pp. 271–285. Springer, Berlin (2003)

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

    Article  MATH  MathSciNet  Google Scholar 

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

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

  39. van Emde Boas, P.: Preserving order in a forest in less than logarithmic time and linear space. Inf. Process. Lett. 6(3), 80–82 (1977)

    Article  MATH  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors would like to thank Mike Codish for all the fruitful discussions on sorting networks and Pierre Letouzey for helping with the extraction mechanism and giving suggestions on how to improve the performance of the extracted code.

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Southern Denmark, Campusvej 55, 5230, Odense M, Denmark

    Luís Cruz-Filipe, Kim S. Larsen & Peter Schneider-Kamp

Authors
  1. Luís Cruz-Filipe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kim S. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luís Cruz-Filipe.

Additional information

Partially supported by the Danish Council for Independent Research, Natural Sciences, Grant DFF-1323-00247.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Cruz-Filipe, L., Larsen, K.S. & Schneider-Kamp, P. Formally Proving Size Optimality of Sorting Networks. J Autom Reasoning 59, 425–454 (2017). https://doi.org/10.1007/s10817-017-9405-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-017-9405-9

Keywords

Mathematics Subject Classification

Search

Navigation