DiVinE 2.0: High-Performance Model Checking

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. s. 31-32. ISBN 978-0-7695-3809-9. 2009.

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

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ů