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”

opaal: A Lattice Model Checker

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00067342" target="_blank" >RIV/00216224:14330/11:00067342 - isvavai.cz</a>

  • Výsledek na webu

    <a href="http://dx.doi.org/10.1007/978-3-642-20398-5" target="_blank" >http://dx.doi.org/10.1007/978-3-642-20398-5</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-642-20398-5" target="_blank" >10.1007/978-3-642-20398-5</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    opaal: A Lattice Model Checker

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

    We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction by using a method similar to Counter-Example Guided Abstraction Refinement. The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features. We report on the status of the first public release of opaal, and demonstrate how opaal can be used for efficient verification on examples from domains such as database programs, lossy communication protocols and cache analysis.

  • Název v anglickém jazyce

    opaal: A Lattice Model Checker

  • Popis výsledku anglicky

    We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction by using a method similar to Counter-Example Guided Abstraction Refinement. The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features. We report on the status of the first public release of opaal, and demonstrate how opaal can be used for efficient verification on examples from domains such as database programs, lossy communication protocols and cache analysis.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

    IN - Informatika

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

  • Návaznosti

    Z - Vyzkumny zamer (s odkazem do CEZ)

Ostatní

  • Rok uplatnění

    2011

  • 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 statě ve sborníku

    Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11)

  • ISBN

    9783642203978

  • ISSN

    0302-9743

  • e-ISSN

  • Počet stran výsledku

    7

  • Strana od-do

    487-493

  • Název nakladatele

    Springer-Verlag

  • Místo vydání

    Neuveden

  • Místo konání akce

    USA

  • Datum konání akce

    1. 1. 2011

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

    WRD - Celosvětová akce

  • Kód UT WoS článku