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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008, p. 234-239. ISBN 978-3-540-88386-9.

Basic information

Original name

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

Name in Czech

DiVinE Multi-Core -- Paralelní nástroj pro ověřování modelu LTL

Authors

BARNAT, Jiří (203 Czech Republic, guarantor), Luboš BRIM (203 Czech Republic) and Petr ROČKAI (203 Czech Republic)

Edition

Berlin / Heidelberg, Automated Technology for Verification and Analysis, p. 234-239, 6 pp. 2008

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Republic of Korea

Confidentiality degree

není předmětem státního či obchodního tajemství

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/08:00024321

Organization unit

Faculty of Informatics

ISBN

978-3-540-88386-9

ISSN

UT WoS

000261873000019

Keywords in English

LTL Model Checking; Parallel; Tool

Tags

LTL model checking, parallel, tool

Tags

International impact, Reviewed

---

Abstract

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.

In Czech

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

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science