Verification of heap manipulating programs with ordered data by extended forest automata
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU117007" target="_blank" >RIV/00216305:26230/15:PU117007 - isvavai.cz</a>
Výsledek na webu
<a href="http://link.springer.com/article/10.1007%2Fs00236-015-0235-0" target="_blank" >http://link.springer.com/article/10.1007%2Fs00236-015-0235-0</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s00236-015-0235-0" target="_blank" >10.1007/s00236-015-0235-0</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Verification of heap manipulating programs with ordered data by extended forest automata
Popis výsledku v původním jazyce
We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.
Název v anglickém jazyce
Verification of heap manipulating programs with ordered data by extended forest automata
Popis výsledku anglicky
We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2015
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ů
Údaje specifické pro druh výsledku
Název periodika
Acta Informatica
ISSN
0001-5903
e-ISSN
1432-0525
Svazek periodika
53
Číslo periodika v rámci svazku
4
Stát vydavatele periodika
DE - Spolková republika Německo
Počet stran výsledku
29
Strana od-do
357-385
Kód UT WoS článku
000376978100003
EID výsledku v databázi Scopus
2-s2.0-84928978668