Can Flash Memory Help in Model Checking?
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F09%3A00028658" target="_blank" >RIV/00216224:14330/09:00028658 - isvavai.cz</a>
Alternative codes found
RIV/00216224:14330/09:00065776
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Can Flash Memory Help in Model Checking?
Original language description
As flash media become common and their capacities and speed grow, they are becoming a practical alternative for standard mechanical drives. So far, external memory model checking algorithms have been optimized for mechanical hard disks corresponding to the model of Aggarwal and Vitter. Since flash memories are essentially different, the model of Aggarwal and Vitter no longer describes their typical behavior. On such a different device, algorithms can have different complexity, which may lead to the design of completely new flash-memory-efficient algorithms. We provide a model for computation of I/O complexity on the model of Aggarwal and Vitter modified for flash memories. We discuss verification algorithms optimized for this model and compare the performance of these algorithms with approaches known from I/O efficient model checking on mechanical hard disks.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2009
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Formal Methods for Industrial Critical Systems
ISBN
978-3-642-03239-4
ISSN
0302-9743
e-ISSN
—
Number of pages
16
Pages from-to
—
Publisher name
Springer Berlin / Heidelberg
Place of publication
Neuveden
Event location
L'Aquila, Italy
Event date
Jan 1, 2008
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
000270704100010