Skip to main content
SpringerLink
Log in

Proof Pearl: The KeY to Correct and Stable Sorting

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

Abstract

We discuss a proof of the correctness of two sorting algorithms: Counting sort and Radix sort. The semi-automated proof is formalized in the state-of-the-art theorem prover KeY.

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

Access this article

Log in via an institution

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

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES ’12, pp. 145–154. ACM, New York (2012). doi:10.1145/2388936.2388960

  2. Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd Edn. Texts in Computer Science. Springer-Verlag (2009). 502 pp, ISBN 978-1-84882-744-8

  3. Apt, K.R., de Boer, F.S., Olderog, E.R., de Gouw, S.: Verification of Object-Oriented programs: A transformational approach. J. Comput. Syst. Sci. 78(3), 823–852 (2012)

    Article  MATH  Google Scholar 

  4. Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Secure information flow for Java. A Dynamic Logic approach. Karlsruhe reports in informatics; 2013-10, KIT (2013). http://digbib.ubka.uni-karlsruhe.de/volltexte/1000036786

  5. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, vol. 4334. Springer (2007)

  6. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transfer 7(3), 212–232 (2005)

    Article  Google Scholar 

  7. Filliâtre, J.C., Magaud, N.: Certification of sorting algorithms in the system Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends. Nice, France (1999). http://www.lri.fr/filliatr/ftp/publis/Filliatre-Magaud.ps.gz

  8. Foley, M., Hoare, C.A.R.: Proof of a recursive program: Quicksort. Comput. J. 14(4), 391–395 (1971)

    Article  MathSciNet  MATH  Google Scholar 

  9. Mostowski, W.: Formalisation and verification of Java Card security properties in Dynamic Logic. In: M. Cerioli (ed.) Proceedings Fundamental Approaches to Software Engineering (FASE), Edinburgh, Lecture Notes in Computer Science, vol. 3442, pp. 357–371. Springer (2005). http://www.springerlink.com/link.asp?id=x0u5bj47bcqhy4b7

  10. Mostowski, W.: Fully verified Java Card API reference implementation. In: VERIFY (2007)

  11. Sternagel, C.: Proof Pearl - A mechanized proof of GHC’s mergesort. J. Autom. Reasoning 51(4), 357–370 (2013)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIACS – Leiden University, Leiden, Netherlands

    Stijn de Gouw, Frank de Boer & Jurriaan Rot

  2. CWI, Amsterdam, Netherlands

    Stijn de Gouw, Frank de Boer & Jurriaan Rot

Authors
  1. Stijn de Gouw
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jurriaan Rot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jurriaan Rot.

Rights and permissions

Reprints and permissions

About this article

Cite this article

de Gouw, S., de Boer, F. & Rot, J. Proof Pearl: The KeY to Correct and Stable Sorting. J Autom Reasoning 53, 129–139 (2014). https://doi.org/10.1007/s10817-013-9300-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-013-9300-y

Keywords

Search

Navigation