Publication Details
Verification of Programs with Complex Data Structures
Formal verification, model checking, infinite state-space systems, regular tree languages, automated abstraction, shape analysis, termination checking.
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.
@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" }