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”

Compositional Entailment Checking for a Fragment of Separation Logic

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU126445" target="_blank" >RIV/00216305:26230/17:PU126445 - isvavai.cz</a>

  • Výsledek na webu

    <a href="http://www.fit.vutbr.cz/research/pubs/all.php?id=11504" target="_blank" >http://www.fit.vutbr.cz/research/pubs/all.php?id=11504</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/s10703-017-0289-4" target="_blank" >10.1007/s10703-017-0289-4</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Compositional Entailment Checking for a Fragment of Separation Logic

  • Popis výsledku v původním jazyce

    We present a decision procedure for checking entailment between separation logic formulas with inductive predicates specifying complex data structures corresponding to finite nesting of various kinds of singly linked lists: acyclic or cyclic, nested lists, skip lists, etc. The decision procedure is compositional in the sense that it reduces the problem of checking entailment between two arbitrary formulas to the problem of checking entailment between a formula and an atom. Subsequently, in case the atom is a predicate, we reduce the entailment to testing membership of a tree derived from the formula in the language of a tree automaton derived from the predicate. The procedure is later also extended to doubly linked lists. We implemented this decision procedure and tested it successfully on verification conditions obtained from programs using both singly and doubly linked nested lists as well as skip lists.

  • Název v anglickém jazyce

    Compositional Entailment Checking for a Fragment of Separation Logic

  • Popis výsledku anglicky

    We present a decision procedure for checking entailment between separation logic formulas with inductive predicates specifying complex data structures corresponding to finite nesting of various kinds of singly linked lists: acyclic or cyclic, nested lists, skip lists, etc. The decision procedure is compositional in the sense that it reduces the problem of checking entailment between two arbitrary formulas to the problem of checking entailment between a formula and an atom. Subsequently, in case the atom is a predicate, we reduce the entailment to testing membership of a tree derived from the formula in the language of a tree automaton derived from the predicate. The procedure is later also extended to doubly linked lists. We implemented this decision procedure and tested it successfully on verification conditions obtained from programs using both singly and doubly linked nested lists 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í

    2017

  • 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

    FORMAL METHODS IN SYSTEM DESIGN

  • ISSN

    0925-9856

  • e-ISSN

    1572-8102

  • Svazek periodika

    2017

  • Číslo periodika v rámci svazku

    51

  • Stát vydavatele periodika

    US - Spojené státy americké

  • Počet stran výsledku

    33

  • Strana od-do

    575-607

  • Kód UT WoS článku

    000416332700007

  • EID výsledku v databázi Scopus

    2-s2.0-85026808268