{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:20:25Z","timestamp":1768004425358,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540727323","type":"print"},{"value":"9783540727347","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72734-7_26","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T05:40:50Z","timestamp":1183009250000},"page":"363-378","source":"Crossref","is-referenced-by-count":11,"title":["Verifying Balanced Trees"],"prefix":"10.1007","author":[{"given":"Zohar","family":"Manna","sequence":"first","affiliation":[]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[]},{"given":"Ting","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"26_CR1","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0743-1066(95)00033-G","volume":"24","author":"R. Backofen","year":"1995","unstructured":"Backofen, R.: A complete axiomatization of a theory with feature and arity constraints. Journal of Logical Programming\u00a024(1-2), 37\u201371 (1995)","journal-title":"Journal of Logical Programming"},{"key":"26_CR2","unstructured":"Baldan, P., Corradini, A., Esparza, J., Heindel, T., K\u00f6nig, 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\u201905 (2005)"},{"key":"26_CR3","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/1040305.1040328","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"C. Calcagno","year":"2005","unstructured":"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\u2013282. ACM Press, New York (2005)"},{"key":"26_CR4","unstructured":"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"},{"issue":"2","key":"26_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"key":"26_CR6","first-page":"91","volume-title":"Machine Intelligence, vol. 7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, vol. 7, pp. 91\u201399. Elsevier, New York (1972)"},{"key":"26_CR7","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. The MIT Press, Cambridge (2001)"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"J. Downey","year":"1980","unstructured":"Downey, J., Sethi, R., Tarjan, R.E.: Variations of the common subexpression problem. Journal of the ACM\u00a027, 758\u2013771 (1980)","journal-title":"Journal of the ACM"},{"key":"26_CR9","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (2001)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/11691372_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Habermehl","year":"2006","unstructured":"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.\u00a03920, pp. 350\u2013364. Springer, Heidelberg (2006)"},{"key":"26_CR11","first-page":"291","volume-title":"Proceedings of 15th IEEE Symposium on Logic in Computer Science","author":"K. Korovin","year":"2000","unstructured":"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\u2013302. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"979","DOI":"10.1007\/3-540-48224-5_79","volume-title":"Automata, Languages and Programming","author":"K. Korovin","year":"2001","unstructured":"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.\u00a02076, pp. 979\u2013992. Springer, Heidelberg (2001)"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LICS.2003.1210049","volume-title":"Proceedings of 18th IEEE Symposium on Logic in Computer Science","author":"V. Kuncak","year":"2003","unstructured":"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\u2013107. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"26_CR14","first-page":"348","volume-title":"Proceedings of the 3rd IEEE Symposium on Logic in Computer Science","author":"M.J. Maher","year":"1988","unstructured":"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\u2013357. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"26_CR15","first-page":"262","volume-title":"The Metamathematics of Algebraic Systems, Collected Papers","author":"A.I. Mal\u2019cev","year":"1971","unstructured":"Mal\u2019cev, A.I.: Axiomatizable classes of locally free algebras of various types. In: The Metamathematics of Algebraic Systems, Collected Papers, pp. 262\u2013281. North-Holland, Amsterdam (1971)"},{"issue":"2","key":"26_CR16","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"3","key":"26_CR17","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the ACM\u00a027(3), 403\u2013411 (1980)","journal-title":"Journal of the ACM"},{"key":"26_CR18","first-page":"320","volume-title":"Proceedings of the 10th Annual Symposium on Theory of Computing","author":"C.R. Reddy","year":"1978","unstructured":"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\u2013325. ACM Press, New York (1978)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-540-27864-1_18","volume-title":"Static Analysis","author":"R. Rugina","year":"2004","unstructured":"Rugina, R.: Quantitative shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 228\u2013245. Springer, Heidelberg (2004)"},{"issue":"2","key":"26_CR20","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T. Rybina","year":"2001","unstructured":"Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Transactions on Computational Logic\u00a02(2), 155\u2013181 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"26_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-540-25984-8_9","volume-title":"Automated Reasoning","author":"T. Zhang","year":"2004","unstructured":"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.\u00a03097, pp. 152\u2013167. Springer, Heidelberg (2004)"},{"key":"26_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/11532231_10","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Zhang","year":"2005","unstructured":"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.\u00a03632, pp. 131\u2013148. Springer, Heidelberg (2005)"},{"key":"26_CR23","doi-asserted-by":"publisher","first-page":"1526","DOI":"10.1016\/j.ic.2006.03.004","volume":"204","author":"T. Zhang","year":"2006","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Information and Computation\u00a0204, 1526\u20131574 (2006)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72734-7_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,16]],"date-time":"2021-08-16T01:36:04Z","timestamp":1629077764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72734-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727323","9783540727347"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72734-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}