Amortized Complexity

swMATH ID: 28606
Software Authors: Tobias Nipkow
Description: Amortized Complexity Verified. A framework for the analysis of the amortized complexity of functional data structures is formalized in Isabelle/HOL and applied to a number of standard examples and to the folowing non-trivial ones: skew heaps, splay trees, splay heaps and pairing heaps. A preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here.
Homepage: https://www.isa-afp.org/entries/Amortized_Complexity.html
Dependencies: Isabelle
Related Software: Isabelle/HOL; Archive Formal Proofs; HOL; Isabelle; Coq; Root Balanced Tree; Density Compiler; Random BSTs; Treaps; QuickSort Cost; CryptHOL; Ergodic theory; Splay Tree; ACE; OCaml; Separation Logic; Isar; TcT; OptiMathSAT; TiML
Cited in: 8 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Amortized complexity verified. Zbl 1465.68059
Nipkow, Tobias

Citations by Year