| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/11:00049765 |
| Název v původním jazyce | CUDA Accelerated LTL Model Checking - Revisited |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2011 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů |
| Počet výskytů výsledku | 1 |
| Údaje z Hodnocení výsledků výzkumných organizací 2014 |
| Výsledek byl hodnocen v Pilíři I |
| Rozsah vyřazení výsledku | Tento výskyt výsledku není vyřazen |
| Zařazení výsledku v hodnocení | neu - Výsledky bez bodového hodnocení nebo vyřazené |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Článek ve sborníku má uvedeno ISBN nebo ISSN, ale to není v databázi Conference Proceedings Citation Index ani v databázi Scopus. |
| Rozdělení výsledku mezi předkladatele |
| Organizace | Výzkumná organizace? | Podíl | Body | Body (upravené podle přílohy č. 8 Metodiky) |
|---|
| Masarykova univerzita / Fakulta informatiky | ano | 100,0 % | 0,000 | |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 2 |
| Počet domácích tvůrců | 2 |
| Tvůrce | Bauch Petr (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5736935) |
| Tvůrce | Češka Milan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 1846000) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | Recently, the massively parallel architecture has been used to significantly accelerate many computation demanding tasks. For example, in [Baier, Kateon, The MIT Press, 2009; Barnat, Brim, Ceska, ICPADS 2009] we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. In this paper we redesign the One-Way-Catch-Them-Young (OWCTY) algorithm [Cerna, Pelanek, SPIN'03] in order to devise a new CUDA accelerated OWCTY algorithm that will significantly outperform the original CUDA accelerated algorithm and will be resistant to slowdown caused by improper ordering of the input data representation. |
| Klíčová slova | Linear Temporal Logic (LTL) Model Checking; massively parallel architecture; One Way Catch Them Young (OWCTY) algorithm |
| Rozsah stran | 1-8 |
| Název sborníku | Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers |
| ISSN | 2190-6807 |
| ISBN | 978-3-939897-22-4 |
| Počet stran výsledku | 8 |
| Název nakladatele | Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik |
| Místo vydání | Dagstuhl, Germany |
| Místo konání akce | Dagstuhl, Germany |
| Rok konání akce | 2011 |
| Typ akce podle státní příslušnoti účastníků | CST - Celostátní |
| Údaje o tomto záznamu o výsledku |
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
| Dodavatel | GA0 - Grantová agentura České republiky (GA ČR) |
| Rok sběru | 2012 |
| Systémové označení dodávky dat | RIV12-GA0-14330___/02:1 |
| Specifikace | RIV/00216224:14330/11:00049765!RIV12-GA0-14330___ |
| Kontrolní kód | [441913A8AC59] |
| Jiný výskyt tohoto výsledku se v RIV nenachází |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | GA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009-2011, GA0/GA) |
| Projekt | GD102/09/H042 - Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů (2009-2012, GA0/GD) |