R 2009

DiVinE Cuda

BARNAT, Jiří, Luboš BRIM, Petr BAUCH, Milan ČEŠKA, Tomáš LAMR et. al.

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

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í

Odkazy

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

Příznaky

Mezinárodní význam
Změněno: 2. 2. 2011 09:39, prof. RNDr. Luboš Brim, CSc.

Anotace

V originále

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.

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