Automata-based verification of programs with tree updates

This paper describes a verification framework for Hoare-style pre- and post-conditions of programs manipulating balanced tree-like data structures. Since the considered verification problem is undecidable, we appeal to the standard semi-algorithmic approach in which the user has to provide loop invariants, which are then automatically checked, together with the program pre- and post-conditions. We specify sets of program states, representing tree-like memory configurations, using Tree Automata with Size Constraints (TASC). The main advantage of this new class of tree automata is that they recognise tree languages based on arithmetic reasoning about the lengths of various (possibly all) paths in trees, like, e.g., in AVL trees or red-black trees. TASCs are closed under union, intersection, and complement, and their emptiness problem is decidable. Thus we obtain a class of automata which are an interesting theoretical contribution by itself. Further, we show that, under few restrictions, one can automatically compute the effect of tree-updating program statements on the set of configurations represented by a TASC, which makes TASC a practical verification tool. We tried out our approach on the insertion procedure for red-black trees, for which we verified that the output on an arbitrary balanced red-black tree is also a balanced red-black tree.