Sciweavers

ACTA
2010

Automata-based verification of programs with tree updates

14 years 18 days ago
Automata-based verification of programs with tree updates
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...
Peter Habermehl, Radu Iosif, Tomás Vojnar
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where ACTA
Authors Peter Habermehl, Radu Iosif, Tomás Vojnar
Comments (0)