opaal: A Lattice Model Checker (2011)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/11:00067342 |
|---|---|
| Název v anglickém jazyce | opaal: A Lattice Model Checker |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2011 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 1 |
| Počet tvůrců celkem | 6 |
| Počet domácích tvůrců | 1 |
| Výčet všech uvedených jednotlivých tvůrců | Andreas E. Dalsgaard (státní příslušnost: DK - Dánské království) Rene R. Hansen (státní příslušnost: DK - Dánské království) Kenneth Y. Joergensen (státní příslušnost: DK - Dánské království) Kim G. Larsen (státní příslušnost: DK - Dánské království) Mads Chr. Olesen (státní příslušnost: DK - Dánské království) Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057) |
| Popis výsledku v anglické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. |
| Klíčová slova oddělená středníkem | verification; lattice; tool |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/978-3-642-20398-5 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11) |
|---|---|
| ISBN | 9783642203978 |
| ISSN | 0302-9743 |
| 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 | 2011 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2014 |
| Specifikace | RIV/00216224:14330/11:00067342!RIV14-MSM-14330___ |
| Datum poslední aktualizace výsledku | 29.05.2014 |
| Kontrolní číslo | 56536709 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Výzkumný záměr podporovaný MŠMT | MSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005 - 2011) |
|---|