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 spacesystems based on symbolic verification---in particular, we concentrate on the use of theso-called regular tree model checking.As a part of our original contribution, we first presentabstract regular tree model checking (ARTMC), a technique based on a combination of regular treemodel checking with an automated abstraction using the counter-example guided abstraction refinementprinciple. Then, we present our original method for verification of safety properties ofpointer-manipulating procedures. The method uses ARTMC as a verification framework.The method was successfully tested on a set of real-life procedures manipulating dynamicdata structures (such as linked lists, doubly linked lists, trees, etc.) - some of theseprocedures were handled fully automatically for the first time using our approach.Finally, we present our original fully automated methodfor termination proofs for programs manipulating tree-like data structures. The method isbased on a combination of ARTMC with counter automata and it was successfully applied onseveral 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

URL

http://www.fit.vutbr.cz/%7Erogalew/pubs/rogalewicz-PhD-thesis.pdf

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",
  url="http://www.fit.vutbr.cz/%7Erogalew/pubs/rogalewicz-PhD-thesis.pdf"
}