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

Zpět na vědecké spisy