Verifying Balanced Trees

Abstract. Balanced search trees provide guaranteed worst-case time performance and hence they form a very important class of data structures. However, the self-balancing ability comes at a price; balanced trees are more complex than their unbalanced counterparts both in terms of data structure themselves and related manipulation operations. In this paper we present a framework to model balanced trees in decidable first-order theories of term algebras with Presburger arithmetic. In this framework, a theory of term algebras (i.e., a theory of finite trees) is extended with Presburger arithmetic and with certain connecting functions that map terms (trees) to integers. Our framework is flexible in the sense that we can obtain a variety of decidable theories by tuning the connecting functions. By adding maximal path and minimal path functions, we obtain a theory of red-black trees in which the transition relation of tree self-balancing (rotation) operations is expressible. We then show h...

• Type: Conference
• Year: 2007
• Where: LFCS
• Authors: Zohar Manna, Henny B. Sipma, Ting Zhang
• Keywords: Balanced Search Trees, Balanced Trees, LFCS 2007, Red-black Tree