2008
DiVinE Multi-Core -- A Parallel LTL Model-Checker
BARNAT, Jiří, Luboš BRIM a Petr ROČKAIZákladní údaje
Originální název
DiVinE Multi-Core -- A Parallel LTL Model-Checker
Název česky
DiVinE Multi-Core -- Paralelní nástroj pro ověřování modelu LTL
Autoři
BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Petr ROČKAI (203 Česká republika)
Vydání
Berlin / Heidelberg, Automated Technology for Verification and Analysis, od s. 234-239, 6 s. 2008
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Korejská republika
Utajení
není předmětem státního či obchodního tajemství
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/08:00024321
Organizační jednotka
Fakulta informatiky
ISBN
978-3-540-88386-9
ISSN
UT WoS
000261873000019
Klíčová slova anglicky
LTL Model Checking; Parallel; Tool
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 30. 3. 2010 09:14, prof. RNDr. Jiří Barnat, Ph.D.
V originále
We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically for multi-core and multi-cpu environments using shared memory. We show how the parallel algorithms allow the tool to exploit the power of contemporary hardware, which is based on increasing number of CPU cores in a single system, as opposed to increasing speed of a single CPU core.
Česky
V tomto článku prezentujeme nástro pro paralelní ověřování modelu v paralelním prostředí se sdílenou pamětí. Nástroj je založen na algoritmech použivaných v prostředí s distribuovanou pamětí, ale tyto efektivně reimplementuje v prostředí se sdílenou pamětí. Smyslem nástroje je demonstrovat způsob, kterým lze zcela využít sílu soudobého HW, jmenovitě nových více=jádrových procesorů.
Návaznosti
| GA201/06/1338, projekt VaV |
| ||
| 1ET408050503, projekt VaV |
| ||
| 1M0545, projekt VaV |
|