Detail publikace

Verification of Programs with Complex Data Structures

ROGALEWICZ, A.

Originální název

Verification of Programs with Complex Data Structures

Typ

kniha odborná

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

ROGALEWICZ, A.

Vydáno

21. 12. 2007

Místo

Brno

ISBN

978-80-214-3548-3

Strany počet

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