Paper Info
Title
Automatic Functional Correctness Proofs For Functional Search Trees
Abstract
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 and 2-3-4 trees, 1-2 brother trees, AA trees and splay trees.
Year
DOI
Venue
2016
10.1007/978-3-319-43144-4_19
INTERACTIVE THEOREM PROVING (ITP 2016)
Field
DocType
Volume
HOL,Discrete mathematics,Tree traversal,AVL tree,Splay tree,Computer science,Correctness,Binary tree,Binary search tree,Search tree
Conference
9807
ISSN
Citations 
PageRank 
0302-9743
2
0.37
References 
Authors
9
1
Name
Order
Citations
PageRank
Tobias Nipkow13056232.28