Automatic Functional Correctness Proofs for Functional Search Trees
In a new approach, functional correctness specifications of insert/update and delete operations on search trees are expressed on the level of lists by means of an inorder traversal function that projects trees to lists. With the help of a small lemma library, functional correctness and preservation of the search tree property are proved automatically (in Isabelle/HOL) for a range of data structures: unbalanced binary trees, AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees.
pdf
BibTeX:
@inproceedings{Nipkow-ITP16,
author={Tobias Nipkow},
title={Automatic Functional Correctness Proofs for Functional Search Trees},
booktitle={Interactive Theorem Proving (ITP 2016)},
editor={J. Blanchette and S. Merz},
publisher=Springer,series=LNCS,volume={9807},pages={307-322},year=2016}
Isabelle theories