DiVinE Multi-Core -- A Parallel LTL Model-Checker

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. s. 234-239. ISBN 978-3-540-88386-9. 2008.

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

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 VaV: Název: Automatizovaná verifikace softwaru

Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru

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

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky