Faculty of Information Technology, BUT

Publication Details

Automata-based Verification of Programs with Tree Updates

HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3920. Berlin: Springer Verlag, 2006, pp. 350-364. ISBN 978-3-540-33056-1.
Czech title
Verifikace programů s operacemi nad vyváženými stromy s využitím automatů
Type
conference paper
Language
english
Authors
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
Formal verification, symbolic verification, programs handling balanced trees, theory of automata.
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.
Published
2006
Pages
350-364
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
3920
Conference
The European Joint Conference on Theory and Practice of Software -- ETAPS'06 / 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems -- TACAS'06, Vienna, AT
ISBN
978-3-540-33056-1
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB8022,
   author = "Peter Habermehl and Radu Iosif and Tom\'{a}\v{s} Vojnar",
   title = "Automata-based Verification of Programs with Tree Updates",
   pages = "350--364",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 3920,
   year = 2006,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-33056-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8022"
}
Back to top