Automata-based Verification of Programs with Tree Updates

This paper describes an effective verification procedure for imperativeprograms that handle (balanced) tree-like data structures. Since theverification problem considered is undecidable, we appeal to aclassical semi-algorithmic approach in which the user has to providemanually the loop invariants in order to check the validity of Hoaretriples of the form $\{P\}C\{Q\}$, where $P, Q$ are the sets of statescorresponding to the pre- and post-conditions, and $C$ is the programto be verified. We specify the sets of states (representing tree-likememory configurations) using  a special class of tree automatanamed Tree Automata with Size Constraints (TASC). The main advantage ofusing TASC in program specifications is that they recognize non-regularsets of treelanguages such as the {\em AVL trees}, the  {\em red-black trees},and in general, specifications involving arithmetic reasoning about thelengths (depths) of various (possibly all) paths in the tree. The classof TASC is closed under the operations of union, intersection andcomplement, and moreover, the emptiness problem is decidable, whichmakes it a practical verification tool. We validate our approachconsidering red-black trees and the insertion procedure, for which weverify that the output of the insertion algorithm is a {\em balanced}red-black tree, i.e. the longest path is at most twice as long as theshortest path.