BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE 2.0: High-Performance Model Checking. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009, s. 31-32. ISBN 978-0-7695-3809-9. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | DiVinE 2.0: High-Performance Model Checking |
Název česky | DiVinE 2.0: Vysokovýkonostní nástroj pro ověřování modelu |
Autoři | BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí). |
Vydání | Los Alamitos (California), International Workshop on High Performance Computational Systems Biology, od s. 31-32, 2 s. 2009. |
Nakladatel | IEEE Computer Society |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Itálie |
Utajení | není předmětem státního či obchodního tajemství |
Forma vydání | tištěná verze "print" |
Kód RIV | RIV/00216224:14330/09:00028659 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-0-7695-3809-9 |
UT WoS | 000275038300004 |
Klíčová slova česky | Ověřování modelu; LTL |
Klíčová slova anglicky | LTL Model Checking |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: RNDr. Petr Ročkai, Ph.D., učo 139761. Změněno: 18. 2. 2013 12:43. |
Anotace |
---|
We present a tool for parallel enumerative LTL model-checking and reachability analysis. The tool brings model checking to high-powered multi-core systems, as well as high-performance clusters. Boasting pluggable modelling language framework, it is possible to leverage the available parallel algorithms for multiple problem domains, by using suitable input language. |
Anotace česky |
---|
V článku je představen nástroj pro paralelní enumerativní ověřování modelu LTL. Ve své aktuální verzi 2.0 je nástroj schopen efektivně využít HW platformu klastr výpočetních vícejádrových uzlů. |
Návaznosti | |
---|---|
GA201/09/1389, projekt VaV | Název: Verifikace a analýza velmi velkých počítačových systémů |
Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů | |
GP201/09/P497, projekt VaV | Název: Automatizovaná formální verifikace s využitím soudobého hardware |
Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů |