Verified Analysis of Functional Data Structures

Author Tobias Nipkow

Thumbnail PDF


  • Filesize: 262 kB
  • 2 pages

Document Identifiers

Author Details

Tobias Nipkow

Cite AsGet BibTex

Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.
  • Program Verification
  • Algorithm Analysis
  • Functional Programming


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Martin Avanzini, Georg Moser, and Michael Schaper. TcT: Tyrolean Complexity Tool. In M. Chechik and J.-F. Raskin, editors, TACAS, volume 9636 of LNCS, pages 407-423. Springer, 2016. Google Scholar
  2. Hauke Brinkop. Verifikation der amortisierten Laufzeit von Pairing Heaps in Isabelle. Bachelor’s thesis, Fakultät für Informatik, Technische Universität München, 2015. Google Scholar
  3. Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In C. Urban and X. Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 137-153. Springer, 2015. Google Scholar
  4. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14, 2012. Google Scholar
  5. Tobias Nipkow. Amortized complexity verified. Archive of Formal Proofs, 2014., Formal proof development.
  6. Tobias Nipkow. Amortized complexity verified. In C. Urban and X. Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 310-324. Springer, 2015. Google Scholar
  7. Tobias Nipkow. Automatic functional correctness proofs for functional search trees. In J. Blanchette and S. Merz, editors, ITP 2016, LNCS. Springer, 2015. To appear. Google Scholar
  8. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL:
  9. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  10. Lars Noschinski, Fabian Emmes, and Jürgen Giesl. Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning, 51(1):27-56, 2013. Google Scholar
  11. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. Puschner, Jan Staschulat, and Per Stenström. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008. Google Scholar