Scalable Multi-core LTL Model-Checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00019427" target="_blank" >RIV/00216224:14330/07:00019427 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Scalable Multi-core LTL Model-Checking
Original language description
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.
Czech name
Škálovatelné LTL ověřování modelu s využitím multi-core
Czech description
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í modelus 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í.

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)