Journal articleHABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automatabased Verification of Programs with Tree Updates. Acta Informatica. 2010, vol. 47, no. 1, pp. 131. ISSN 00015903.  Publication language:  english 

Original title:  Automatabased Verification of Programs with Tree Updates 

Title (cs):  Verifikace programů s operacemi nad vyváženými stromy s využitím automatů 

Pages:  131 

Place:  DE 

Year:  2010 

Journal:  Acta Informatica, Vol. 47, No. 1, DE 

ISSN:  00015903 

URL:  http://www.springerlink.com/content/l76231376151vx88/ [HTML] 

Keywords 

Formal verification, symbolic verification, programs handling balanced trees, theory of automata. 
Annotation 

This paper, which is an extended version of a paper originally published at TACAS'06, describes an effective verification procedure for imperative
programs that handle (balanced) treelike data structures. Since the
verification problem considered is undecidable, we appeal to a
classical semialgorithmic 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 postconditions, and C is the program to
be verified. We specify the sets of states (representing treelike
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 nonregular
sets of tree languages such as the AVL trees, the redblack 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 redblack trees and the insertion procedure, for which we
verify that the output of the insertion algorithm is a balanced redblack tree, i.e. the longest path is at most twice as long as the shortest path. 
BibTeX: 

@ARTICLE{
author = {Peter Habermehl and Radu Iosif and Tom{\'{a}}{\v{s}} Vojnar},
title = {Automatabased Verification of Programs with Tree Updates},
pages = {131},
journal = {Acta Informatica},
volume = {47},
number = {1},
year = {2010},
ISSN = {00015903},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9166}
} 
