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

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

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

V originále

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.

Č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ů