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 how to reduce the verification problem of the red-black tree algorithm to constraint satisfiability problems in the extended theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Backofen, R.: A complete axiomatization of a theory with feature and arity constraints. Journal of Logical Programming 24(1-2), 37–71 (1995)
Baldan, P., Corradini, A., Esparza, J., Heindel, T., König, B., Kozioura, V.: Verifying red-black trees. In: Proceedings of the 1st International Workshop on the Verification of Concurrent Systems with Dynamic Allocated Heaps, COSMICAH’05 (2005)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 271–282. ACM Press, New York (2005)
Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2002), Electronic edition at http://l3ux02.univ-lille3.fr/tata/tata.pdf
Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation 112(2), 167–216 (1994)
Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, vol. 7, pp. 91–99. Elsevier, New York (1972)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. The MIT Press, Cambridge (2001)
Downey, J., Sethi, R., Tarjan, R.E.: Variations of the common subexpression problem. Journal of the ACM 27, 758–771 (1980)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (2001)
Habermehl, P., Iosif, R., Vojnar, T.: Automata-based verification of programs with tree updates. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 350–364. Springer, Heidelberg (2006)
Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In: Proceedings of 15th IEEE Symposium on Logic in Computer Science, pp. 291–302. IEEE Computer Society Press, Los Alamitos (2000)
Korovin, K., Voronkov, A.: Knuth-Bendix constraint solving is NP-complete. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 979–992. Springer, Heidelberg (2001)
Kuncak, V., Rinard, M.: The structural subtyping of non-recursive types is decidable. In: Proceedings of 18th IEEE Symposium on Logic in Computer Science, pp. 96–107. IEEE Computer Society Press, Los Alamitos (2003)
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite tree. In: Proceedings of the 3rd IEEE Symposium on Logic in Computer Science, pp. 348–357. IEEE Computer Society Press, Los Alamitos (1988)
Mal’cev, A.I.: Axiomatizable classes of locally free algebras of various types. In: The Metamathematics of Algebraic Systems, Collected Papers, pp. 262–281. North-Holland, Amsterdam (1971)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM 27(2), 356–364 (1980)
Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the ACM 27(3), 403–411 (1980)
Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: Proceedings of the 10th Annual Symposium on Theory of Computing, pp. 320–325. ACM Press, New York (1978)
Rugina, R.: Quantitative shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 228–245. Springer, Heidelberg (2004)
Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Transactions on Computational Logic 2(2), 155–181 (2001)
Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 152–167. Springer, Heidelberg (2004)
Zhang, T., Sipma, H.B., Manna, Z.: The decidability of the first-order theory of term algebras with Knuth-Bendix order. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 131–148. Springer, Heidelberg (2005)
Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Information and Computation 204, 1526–1574 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Manna, Z., Sipma, H.B., Zhang, T. (2007). Verifying Balanced Trees. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-72734-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72732-3
Online ISBN: 978-3-540-72734-7
eBook Packages: Computer ScienceComputer Science (R0)