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
—