Publication detail

Verification of Programs with Complex Data Structures

ROGALEWICZ, A.

Original Title

Verification of Programs with Complex Data Structures

Type

book

Language

English

Original Abstract

In this thesis, we discuss methods of model checking of infinite-state space systems based on symbolic verification---in particular, we concentrate on the use of the so-called regular tree model checking. As a part of our original contribution, we first present abstract regular tree model checking (ARTMC), a technique based on a combination of regular tree model checking with an automated abstraction using the counter-example guided abstraction refinement principle. Then, we present our original method for verification of safety properties of pointer-manipulating procedures. The method uses ARTMC as a verification framework. The method was successfully tested on a set of real-life procedures manipulating dynamic data structures (such as linked lists, doubly linked lists, trees, etc.) - some of these procedures were handled fully automatically for the first time using our approach. Finally, we present our original fully automated method for termination proofs for programs manipulating tree-like data structures. The method is based on a combination of ARTMC with counter automata and it was successfully applied on several tree manipulating procedures.

Keywords

Formal verification, model checking, infinite state-space systems, regular tree languages, automated abstraction, shape analysis, termination checking.

Authors

ROGALEWICZ, A.

Released

21. 12. 2007

Location

Brno

ISBN

978-80-214-3548-3

Pages count

122

BibTex

@book{BUT61788,
  author="Adam {Rogalewicz}",
  title="Verification of Programs with Complex Data Structures",
  year="2007",
  address="Brno",
  pages="122",
  isbn="978-80-214-3548-3"
}