Flash memory efficient LTL model checking

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00049402" target="_blank" >RIV/00216224:14330/11:00049402 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1016/j.scico.2010.03.005" target="_blank" >http://dx.doi.org/10.1016/j.scico.2010.03.005</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.scico.2010.03.005" target="_blank" >10.1016/j.scico.2010.03.005</a>

Result language

angličtina

Original language name

Flash memory efficient LTL model checking

Original language description

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.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

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

2011

Confidentiality

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

Name of the periodical

Science of Computer Programming

ISSN

0167-6423

e-ISSN

—

Volume of the periodical

76

Issue of the periodical within the volume

2

Country of publishing house

NL - THE KINGDOM OF THE NETHERLANDS

Number of pages

22

Pages from-to

136-157

UT code for WoS article

000285220600006

EID of the result in the Scopus database

—