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) - 2005
2005Buchaufsatz/Kapitel in Sammelwerk
Informatik
Titel:
Verifying Red-Black Trees
Autor*in:
Baldan, Paolo;Corradini, Andrea;Esparza, Javier;Heindel, Tobias;König, BarbaraUDE
GND
1050396502
LSF ID
15982
ORCID
0000-0002-4193-2889ORCID iD
Sonstiges
der Hochschule zugeordnete*r Autor*in
;
Kozioura, Vitali

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. Proceedings available as report RR-05-04 (Queen Mary, University of London)