Baldan, Paolo; Corradini, Andrea; Esparza, Javier; Heindel, Tobias; König, Barbara; Kozioura, Vitali:

Verifying Red-Black Trees

In: Proceedings of the First international workshop on the verification of COncurrent Systems with dynaMIC Allocated Heaps, COSMICAH 2005. - (Technical report of Queen Mary University of London ; RR-05-04)
Buchaufsatz / Kapitel / Fach: Informatik
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.
Proceedings available as report RR-05-04 (Queen Mary, University of London)