BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008. s. 234-239, 6 s. ISBN 978-3-540-88386-9.
Další formáty:   BibTeX LaTeX RIS
Zá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
Originální 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 0302-9743
UT WoS 000261873000019
Klíčová slova anglicky LTL Model Checking; Parallel; Tool
Štítky LTL model checking, parallel, tool
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 30. 3. 2010 09:14.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 28. 9. 2020 21:19