Verified Analysis of Functional Data Structures

Nipkow, Tobias

doi:10.4230/LIPIcs.FSCD.2016.4

File

LIPIcs.FSCD.2016.4.pdf

Filesize: 262 kB
2 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSCD.2016.4
URN: urn:nbn:de:0030-drops-59701

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)
https://doi.org/10.4230/LIPIcs.FSCD.2016.4

Abstract

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.

Keywords

Program Verification
Algorithm Analysis
Functional Programming

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

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.
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.
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.
Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14, 2012.
Tobias Nipkow. Amortized complexity verified. Archive of Formal Proofs, 2014. http://isa-afp.org/entries/Amortized_Complexity.shtml, Formal proof development.
Tobias Nipkow. Amortized complexity verified. In C. Urban and X. Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 310-324. Springer, 2015.
Tobias Nipkow. Automatic functional correctness proofs for functional search trees. In J. Blanchette and S. Merz, editors, ITP 2016, LNCS. Springer, 2015. To appear.
Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
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.
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.