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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F07%3APU70921" target="_blank" >RIV/00216305:26230/07:PU70921 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
Original language description
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.
Czech name
Analýza protipříkladů v abstraktním regulárním model checkingu pro složité dynamické datové struktury
Czech description
Článek studuje použití abstraktního regulárního model checkingu, uvnitř úspěšné metody pro verifikace programů se složitými datovými strukturami, a to zejména analýza protipříkladů.<br>

Project
<a href="/en/project/GD102%2F05%2FH050" target="_blank" >GD102/05/H050: Integrated Approach to Education of PhD Students in the Area of Parallel and Distributed Systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)
ISBN
978-80-7355-077-6
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
59-66
Publisher name
NEUVEDEN
Place of publication
Znojmo
Event location
Znojmo
Event date
Oct 26, 2007
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)