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. p. 234-239. ISBN 978-3-540-88386-9. 2008. |
|
Other formats:
BibTeX
LaTeX
RIS
|
| 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 | |
|---|---|
| Original language | English |
| Type of outcome | Proceedings paper |
| Field of Study | 10201 Computer sciences, information science, bioinformatics |
| Country of publisher | Republic of Korea |
| Confidentiality degree | is not subject to a state or trade secret |
| 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 | 0302-9743 |
| UT WoS | 000261873000019 |
| Keywords in English | LTL Model Checking; Parallel; Tool |
| Tags | LTL model checking, parallel, tool |
| Tags | International impact, Reviewed |
| Changed by | Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 30/3/2010 09:14. |
| Abstract |
|---|
| 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. |
| Abstract (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 | |
PrintDisplayed: 19/4/2024 11:41