Abstract
This paper describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the AVL trees, the red-black trees, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various (possibly all) paths in the tree. The class of TASC is closed under the operations of union, intersection and complement, and moreover, the emptiness problem is decidable, which makes it a practical verification tool. We validate our approach considering red-black trees and the insertion procedure, for which we verify that the output of the insertion algorithm is a balanced red-black tree, i.e. the longest path is at most twice as long as the shortest path.
This work was supported in part by the French Ministry of Research (ACI project Securité Informatique) and the Czech Grant Agency (projects GA CR 102/04/0780 and 102/03/D211).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Madhusudan, P.: Visibly Pushdown Languages. In: Proceedings of STOC 2004. ACM Press, New York (2004)
Baldan, P., Corradini, A., Esparza, J., Heindel, T., König, B., Kozioura, V.: Verifying Red-Black Trees. In: Proc. of COSMICAH (2005)
Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, p. 421. Springer, Heidelberg (1997)
Calcagno, C., Gardner, P., Zarfaty, U.: Context Logic and Tree Update. In: Proceedings of POPL 2005. ACM Press, New York (2005)
Comon, H., Cortier, V.: Tree Automata with One Memory, Set Constraints and Cryptographic Protocols. Theoretical Computer Science 331 (2005)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. Release on October 1, 2002 (1997), Available on http://www.grappa.univ-lille3.fr/tata
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, Cambridge (1990)
Dal Zilio, S., Lugiez, D.: Multitrees Automata, Presburger’s Constraints and Tree Logics. Technical Report 08-2002, LIF (2002)
Geidmanis, D.: Unsolvability of the Emptiness Problem for Alternating 1-way Multi-head and Multi-tape Finite Automata over Single-letter Alphabet. In: Computers and Artificial Intelligence, vol. 10 (1991)
Habermehl, P., Iosif, R., Vojnar, T.: Automata-based Verification of Programs with Tree Updates. Technical Report TR-2005-16, Verimag (2005)
Moeller, A., Schwartzbach, M.: The Pointer Assertion Logic Engine. In: Proceeedings of PLDI 2001. ACM Press, New York (2001)
Parduhn, S.: Algorithm Animation Using Shape Analysis with Special Regard to Binary Trees. Technical report, Universit at des Saarlandes (2005)
Petersen, H.: Alternation in Simple Devices. In: Fülöp, Z., Gecseg, F. (eds.) ICALP 1995. LNCS, vol. 944, p. 686. Springer, Heidelberg (1995)
Presburger, M.: Über die Vollstandigkeit eines Gewissen Systems der Arithmetik. Comptes Rendus du I Congr’es des Pays Slaves, Warsaw (1929)
Rabin, M.O.: Decidability of Second Order Theories and Automata on Infinite Trees. Transactions of American Mathematical Society 141 (1969)
Rugina, R.: Quantitative Shape Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 228–245. Springer, Heidelberg (2004)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. TOPLAS 24(3) (2002)
Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in Trees for Free. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1136–1149. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Habermehl, P., Iosif, R., Vojnar, T. (2006). Automata-Based Verification of Programs with Tree Updates. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_23
Download citation
DOI: https://doi.org/10.1007/11691372_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)