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.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2020)
- Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
- Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
- Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2018)
- Nipkow, Tobias: Automatic functional correctness proofs for functional search trees (2016)
- Nipkow, Tobias: Amortized complexity verified (2015)