An assertional proof of the stability and correctness of Natural Mergesort. (English) Zbl 1367.68080


68P10 Searching and sorting
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Roland Backhouse. 1995. The calculational method. Information Processing Letter 53, 3, 121.
[2] Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005 (LNCS), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.), Vol. 4111. Springer, 364–387.
[3] Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter. 2011. Specification and verification: The spec# experience. Communications of the ACM 54, 6 (June 2011), 81–91. · Zbl 05928243
[4] Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. 2013. Secure Information Flow for Java. A Dynamic Logic Approach. Extended Version. Karlsruhe reports in informatics. Fakultät für Informatik.
[5] Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt. 2007. Verification of Object-oriented Software: The KeY Approach. Springer.
[6] Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer. · Zbl 1069.68095
[7] Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009 (LNCS), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 23–42.
[8] Stijn de Gouw, Frank S. de Boer, and Jurriaan Rot. 2014. Proof pearl: The key to correct and stable sorting. Journal of Automated Reasoning 53, 2, 129–139. · Zbl 1314.68277
[9] Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, and Reiner Hähnle. 2015. OpenJDK’s java.utils.Collection.sort() is broken: The good, the bad and the worst case. In Computer Aided Verification. 27th International Conference, CAV 2015 (LNCS). Springer.
[10] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 (LNCS), C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol. 4963. Springer, 337–340.
[11] Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where programs meet provers. In Programming Languages and Systems. 22nd European Symposium on Programming, ESOP 2013 (LNCS), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125–128. · Zbl 1435.68366
[12] Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers.
[13] Donald E. Knuth. 1973. The Art of Computer Programming, Vol. III: Sorting and Searching. Addison-Wesley. · Zbl 0302.68010
[14] Claire Le Goues, K. Rustan M. Leino, and Michał Moskal. 2011. The boogie verification debugger (tool paper). In Software Engineering and Formal Methods. 9th International Conference, SEFM 2011 (LNCS), Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.), Vol. 7041. Springer, 407–414.
[15] K. Rustan and M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In LPAR-16 (LNCS), Edmund M. Clarke and Andrei Voronkov (Eds.), Vol. 6355. Springer, 348–370. · Zbl 1253.68095
[16] K. Rustan and M. Leino. 2012. Automating induction with an SMT solver. In Verification, Model Checking, and Abstract Interpretation. 13th International Conference, VMCAI 2012 (LNCS), Viktor Kuncak and Andrey Rybalchenko (Eds.), Vol. 7148. Springer, 315–331. · Zbl 1326.68262
[17] K. Rustan, M. Leino and Nadia Polikarpova. 2014. Verified calculations. In Verified Software: Theories, Tools, Experiments. 5th International Conference, VSTTE 2013, Revised Selected Papers (LNCS), Ernie Cohen and Andrey Rybalchenko (Eds.), Vol. 8164. Springer, 170–190.
[18] K. Rustan M. Leino, and Valentin Wüstholz. 2014. The Dafny integrated development environment. In Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014 (EPTCS), Catherine Dubois, Dimitra Giannakopoulou, and Dominique Méry (Eds.), Vol. 149. 3–15.
[19] Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer. · Zbl 0994.68131
[20] Christian Sternagel. 2013. Proof pearl: A mechanized proof of GHC’s mergesort. Journal of Automated Reasoning 51, 4, 357–370. · Zbl 1314.68288
[21] Julian Tschannen, Carlo A. Furia, Martin Nordio, and Nadia Polikarpova. 2015. Autoproof: Auto-active functional verification of object-oriented programs. In Tools and Algorithms for the Construction and Analysis of Systems. 21st International Conference, TACAS 2015 (LNCS), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035. Springer, 566–580.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.