"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."@en . . "448947" . "\u0160k\u00E1lovateln\u00E9 LTL ov\u011B\u0159ov\u00E1n\u00ED modelu s vyu\u017Eit\u00EDm multi-core"@cs . "RIV/00216224:14330/07:00019427!RIV08-AV0-14330___" . . . . "[3A35B7576B1C]" . "\u0160k\u00E1lovateln\u00E9 LTL ov\u011B\u0159ov\u00E1n\u00ED modelu s vyu\u017Eit\u00EDm multi-core"@cs . "3"^^ . "14330" . "Scalable Multi-core LTL Model-Checking"@en . . "Lecture Notes in Computer Science" . "Brim, Lubo\u0161" . "3"^^ . "RIV/00216224:14330/07:00019427" . . "Parallel LTL Model Checking; multi-core"@en . "Scalable Multi-core LTL Model-Checking"@en . "4595/2007" . . . "Ro\u010Dkai, Petr" . . "Scalable Multi-core LTL Model-Checking" . . "0302-9743" . "P(1ET408050503), P(1M0545), P(GA201/06/1338), Z(MSM0021622419)" . . . "17"^^ . "-1" . "Barnat, Ji\u0159\u00ED" . "DE - Spolkov\u00E1 republika N\u011Bmecko" . . . "Scalable Multi-core LTL Model-Checking" . . "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." . "187-203" . . "Pokrok ve v\u00FDvoji HW zp\u016Fsobil, \u017Ee v\u00EDce j\u00E1drov\u00E9 syst\u00E9my se sd\u00EDlenou pam\u011Bt\u00ED se staly b\u011B\u017En\u011B dostupn\u00E9. Tyto architektury nab\u00EDzej\u00ED jednotliv\u00FDm aplikac\u00EDm vyu\u017E\u00EDt paralelismu a tak \u0159e\u0161it \u00FAkoly v krat\u0161\u00EDm \u010Dase. Jednou z mo\u017En\u00FDch aplikac\u00ED je probl\u00E9m ov\u011B\u0159ov\u00E1n\u00ED modelu s vyu\u017Eit\u00EDm LTL. V \u010Dl\u00E1nku je pops\u00E1no n\u011Bkolik obecn\u00FDch technik pro v\u00FDvoj aplikac\u00ED, kter\u00E9 umo\u017En\u00ED aplikac\u00EDm l\u00E9pe vyu\u017E\u00EDt mo\u017Enost\u00ED paraleln\u00EDch architektur se sd\u00EDlenou pam\u011Bt\u00ED."@cs . . . . .