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ří; BRIM Luboš; ROČKAI Petr
• Rok publikování: 2008
• Druh: Článek ve sborníku
• Konference: Automated Technology for Verification and Analysis
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: LTL Model Checking; Parallel; Tool
• Popis: 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ů.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Automatizovaná verifikace softwaru