Faculty of Information Technology, BUT

Publication Details

Verification of Programs with Complex Data Structures

ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3.
Czech title
Verifikace programů se složitými datovými strukturami
Type
book
Language
english
Authors
URL
Keywords
Formal verification, model checking, infinite state-space systems, regular tree languages, automated abstraction, shape analysis, termination checking.
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.
Published
2007
Pages
122
ISBN
978-80-214-3548-3
Place
Brno, CZ
BibTeX
@BOOK{FITPUB8522,
   author = "Adam Rogalewicz",
   title = "Verification of Programs with Complex Data Structures",
   pages = 122,
   year = 2007,
   location = "Brno, CZ",
   ISBN = "978-80-214-3548-3",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8522"
}
Back to top