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

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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&nbsp; 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&nbsp; algorithm used for a counterexample analysis and we prove its correctness.

Název v anglickém jazyce

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

Popis výsledku anglicky

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&nbsp; 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&nbsp; algorithm used for a counterexample analysis and we prove its correctness.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GD102%2F05%2FH050" target="_blank" >GD102/05/H050: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

ISBN

978-80-7355-077-6

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

59-66

Název nakladatele

NEUVEDEN

Místo vydání

Znojmo

Místo konání akce

Znojmo

Datum konání akce

26. 10. 2007

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—