Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

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