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

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

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