Publication detail

Automata-based Verification of Programs with Tree Updates

HABERMEHL, P. IOSIF, R. VOJNAR, T.

Original Title

Automata-based Verification of Programs with Tree Updates

Type

article in a collection out of WoS and Scopus

Language

English

Original Abstract

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 program tobe 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 tree languages such as the AVL trees, the  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 balanced red-black tree, i.e. the longest path is at most twice as long as the shortest path.

Keywords

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

Authors

HABERMEHL, P.; IOSIF, R.; VOJNAR, T.

RIV year

2006

Released

29. 3. 2006

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-33056-1

Book

Tools and Algorithms for the Construction and Analysis of Systems

Edition

Lecture Notes in Computer Science

Pages from

350

Pages to

364

Pages count

15

URL

http://www-verimag.imag.fr/TR/TR-2005-16.ps

BibTex

@inproceedings{BUT30893,
  author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}",
  title="Automata-based Verification of Programs with Tree Updates",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2006",
  series="Lecture Notes in Computer Science",
  volume="3920",
  pages="350--364",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-33056-1",
  url="http://www-verimag.imag.fr/TR/TR-2005-16.ps"
}