Verifying Red-Black Trees
Reference
Paolo Baldan, Andrea Corradini, Javier Esparza, Tobias Heindel, Barbara König, and Vitali Kozioura. Verifying red-black trees. In Proc. of COSMICAH '05, 2005. Proceedings available as report RR-05-04 (Queen Mary, University of London).
Abstract
We show how to verify the correctness of insertion of elements into red-black trees—a form of balanced search trees—using analysis techniques developed for graph rewriting. We first model red-black trees and operations on them using hypergraph rewriting. Then we use the tool Augur, which computes approximated unfoldings, in order to show that insertion preserves the property that there are no two consecutive red nodes in a tree, a requirement for red-black trees. Furthermore, we prove that the tree remains balanced by exploiting a type system that can be obtained as an instance of a general framework.
Suggested BibTeX entry:
@inproceedings{BCEHKK05,
author = {Paolo Baldan and Andrea Corradini and Javier Esparza and Tobias Heindel and Barbara K\"onig and Vitali Kozioura},
booktitle = {Proc. of COSMICAH '05},
note = {Proceedings available as report RR-05-04 (Queen Mary, University of London)},
title = {Verifying Red-Black Trees},
year = {2005}
}
