DiVinE 2.0

ROČKAI, Petr, Jiří BARNAT, Luboš BRIM a Milan ČEŠKA. DiVinE 2.0. 2009.

Základní údaje

Originální název

DiVinE 2.0

Název česky

DiVinE 2.0

Autoři

ROČKAI, Petr (703 Slovensko, domácí), Jiří BARNAT (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Milan ČEŠKA (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

URL

Kód RIV

RIV/00216224:14330/09:00028810

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

parallel verification; multi-core; model-checking; cluster; mpi

Technické parametry

Paralelní verifikační nástroj pro ověřování modelů LTL vlastností.

Štítky

cluster, distributed memory, Model-Checking, MPI, multi-core architecture, parallel verification, shared memory

Příznaky

Mezinárodní význam

---

Anotace

V originále

DiVinE 2.0 exploits full power of modern x86 hardware and reduces unnecessary delays in workflow. Employing state-of-the-art parallel liveness checking algorithm, DiVinE 2.0 offers unmatched scalability on both shared memory and distributed memory platforms in the range of 2- to 16-core machines and clusters thereof. Moreover, the tool supports 64-bit platforms out of the box, allowing it to leverage all the memory available in contemporary systems (and systems of the upcoming years).

Česky

DiVinE 2.0 je paralelní nástroj pro verifikaci LTL vlastností. Nástroj používá jak algoritmy pro práci ve sdílené pameti na více-jadrových systémech tak i pro práci v distribuované paměti na víceuzlových výpočetních clusterech.

---

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/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaný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ů