Identifikační kód | RIV/00216224:14330/11:00049402 |
Název v anglickém jazyce | Flash memory efficient LTL model checking |
Druh | J - Článek v odborném periodiku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2011 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 3 |
Počet tvůrců celkem | 5 |
Počet domácích tvůrců | 3 |
Výčet všech uvedených jednotlivých tvůrců | Stefan Edelkamp (státní příslušnost: DE - Spolková republika Německo) Damian Sulewski (státní příslušnost: DE - Spolková republika Německo) Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792) Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) Pavel Šimeček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 4006852) |
Popis výsledku v anglickém jazyce | So far, large-scale LTL model checking algorithms have been designed to employ external memory optimized for magnetic disks. We propose algorithms optimized for flash memory access. In contrast to approaches relying on the delayed detection of duplicatestates, in this work, we design and exploit appropriate hash functions to re-invent immediate duplicate detection. |
Klíčová slova oddělená středníkem | Model checking; External memory algorithms; Algorithm engineering |
Stránka www, na které se nachází výsledek | - |
DOI výsledku | 10.1016/j.scico.2010.03.005 |