Publication detail

Automata-based Verification of Programs with Tree Updates

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

Original Title

Automata-based Verification of Programs with Tree Updates

English Title

Automata-based Verification of Programs with Tree Updates

Type

journal article - other

Language

en

Original Abstract

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) 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.

English abstract

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) 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.

Keywords

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

RIV year

2010

Released

01.02.2010

Publisher

NEUVEDEN

Location

NEUVEDEN

ISBN

0001-5903

Periodical

Acta Informatica

Year of study

47

Number

1

State

DE

Pages from

1

Pages to

31

Pages count

31

URL

Documents

BibTex


@article{BUT50539,
  author="Iosif {Radu} and Tomáš {Vojnar} and Peter {Habermehl}",
  title="Automata-based Verification of Programs with Tree Updates",
  annote="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) 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.",
  address="NEUVEDEN",
  chapter="50539",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  journal="Acta Informatica",
  number="1",
  volume="47",
  year="2010",
  month="february",
  pages="1--31",
  publisher="NEUVEDEN",
  type="journal article - other"
}