Detail publikace

Automata-based Verification of Programs with Tree Updates

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

Originální název

Automata-based Verification of Programs with Tree Updates

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2006

Vydáno

29. 3. 2006

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-33056-1

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science

Strany od

350

Strany do

364

Strany počet

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"
}