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