Scalable Multi-core LTL Model-Checking

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1st ed. Berlin, Heidelberg: Springer-Verlag, 2007, p. 187-203. ISBN 978-3-540-73369-0.

Basic information

Original name

Scalable Multi-core LTL Model-Checking

Name in Czech

Škálovatelné LTL ověřování modelu s využitím multi-core

Authors

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

Edition

1. vyd. Berlin, Heidelberg, Model Checking Software, p. 187-203, 17 pp. 2007

Publisher

Springer-Verlag

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

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/07:00019427

Organization unit

Faculty of Informatics

ISBN

978-3-540-73369-0

ISSN

UT WoS

000247906900013

Keywords in English

Parallel LTL Model Checking; multi-core

Tags

multi-core, Parallel LTL Model Checking

Tags

International impact, Reviewed

---

Abstract

V originále

Recent development in computer hardware has brought more wide-spread emergence of shared-memory, multi-core systems. These architectures offer opportunities to speed up various tasks; among others LTL model checking. In the paper we show a design for a parallel shared memory LTL model checker, that is based on a distributed memory algorithm. To achieve good scalability, we have devised and experimentally evaluated several implementation techniques, which we present in the paper.

In Czech

Pokrok ve vývoji HW způsobil, že více jádrové systémy se sdílenou pamětí se staly běžně dostupné. Tyto architektury nabízejí jednotlivým aplikacím využít paralelismu a tak řešit úkoly v kratším čase. Jednou z možných aplikací je problém ověřování modelu s využitím LTL. V článku je popsáno několik obecných technik pro vývoj aplikací, které umožní aplikacím lépe využít možností paralelních architektur se sdílenou pamětí.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
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