DiVinE Cuda

BARNAT, Jiří, Luboš BRIM, Petr BAUCH, Milan ČEŠKA a Tomáš LAMR. DiVinE Cuda. 2009.

Základní údaje

• Originální název: DiVinE Cuda
• Název česky: DiVinE Cuda
• Autoři: BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, domácí), Milan ČEŠKA (203 Česká republika, domácí) a Tomáš LAMR (203 Česká republika, domácí).
• Vydání: 2009.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Software
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Kód RIV: RIV/00216224:14330/09:00028808
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: masivelly parallel verification; model-checking; CUDA
• Technické parametry: LTL model checker využívající masivně paralelní technologii CUDA
• Štítky: masivelly parallel verification; model-checking; CUDA
• Příznaky: Mezinárodní význam

Anotace

New generation of DiVinE tool allowing for significant acceleration of model checking process by full utilization of modern massively parallel architectures. The tool is effectively utilizing the CUDA technologie.

Anotace česky

Nová generace nástroje DiVinE, která dovoluje efektivní využítí moderních vysoce paralelních architektur pro akceleraci procesu LTL ověřování modelů (LTL Model Checking). Nástroj je zejména určen pro využití technologie CUDA, ktera je široce dostupná v současných grafickách kartách.

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ů

• GD102/09/H042, projekt VaV: Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaný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ů