HOLÍK Lukáš and ROGALEWICZ Adam. Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo: Ing. Zdeněk Novotný, CSc., 2007, pp. 5966. ISBN 9788073550776. 
Publication language:  english 

Original title:  Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures 

Title (cs):  Analýza protipříkladů v abstraktním regulárním model checkingu pro složité dynamické datové struktury 

Pages:  5966 

Proceedings:  Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007) 

Conference:  MEMICS'07  3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science 

Place:  Znojmo, CZ 

Year:  2007 

ISBN:  9788073550776 

Publisher:  Ing. Zdeněk Novotný, CSc. 

URL:  http://www.fit.vutbr.cz/~rogalew/pubs/Memics2007.pdf [PDF] 

Keywords 

Formal verification, Regular tree model checking, shape analysis,

Annotation 

We focus in details on the use of abstract regular tree model checking
(ARTMC) within a successful method for verification of programs with
dynamic data structures. The method is based on a use of a set of
transducers to describe the behaviour of the verified system. But the
ARTMC method was originally developed for systems of one transducer
only and its generalization to several ones was supposed to be
straightforward. Although this straightforward generalization (used in
a prototype implementation) works well in a number of examples, the
counterexample analysis is in general unreliable and can cause infinite
looping of the tool as we demonstrate on a simple example containing an
erroneous pointer manipulation. Therefore we propose a new algorithm
used for a counterexample analysis and we prove its correctness. 
BibTeX: 

@INPROCEEDINGS{
author = {Luk{\'{a}}{\v{s}} Hol{\'{i}}k and Adam Rogalewicz},
title = {Counterexample Analysis in Abstract Regular Tree Model
Checking of Complex Dynamic Data Structures},
pages = {5966},
booktitle = {Third Doctoral Workshop on Mathematical and Engineering
Methods in Computer Science (MEMICS 2007)},
year = {2007},
location = {Znojmo, CZ},
publisher = {Ing. Zden{\v{e}}k Novotn{\'{y}}, CSc.},
ISBN = {9788073550776},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso88592?id=8521}
} 