This HTML5 document contains 51 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n21http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n17http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216224%3A14330%2F09%3A00065776%21RIV14-MSM-14330___/
n23http://purl.org/net/nknouf/ns/bibtex#
n22http://localhost/temp/predkladatel/
n11http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n8http://linked.opendata.cz/resource/domain/vavai/projekt/
n6http://linked.opendata.cz/ontology/domain/vavai/
n18https://schema.org/
n10http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n12http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n14http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n5http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216224%3A14330%2F09%3A00065776%21RIV14-MSM-14330___
rdf:type
n6:Vysledek skos:Concept
dcterms: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. 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.
dcterms:title
Can Flash Memory Help in Model Checking? Can Flash Memory Help in Model Checking?
skos:prefLabel
Can Flash Memory Help in Model Checking? Can Flash Memory Help in Model Checking?
skos:notation
RIV/00216224:14330/09:00065776!RIV14-MSM-14330___
n3:aktivita
n4:P n4:Z
n3:aktivity
P(1ET408050503), P(GA201/06/1338), Z(MSM0021622419)
n3:dodaniDat
n5:2014
n3:domaciTvurceVysledku
n11:5692792 n11:6500773 n11:4006852
n3:druhVysledku
n7:D
n3:duvernostUdaju
n19:S
n3:entitaPredkladatele
n17:predkladatel
n3:idSjednocenehoVysledku
305795
n3:idVysledku
RIV/00216224:14330/09:00065776
n3:jazykVysledku
n14:eng
n3:klicovaSlova
Flash memory; SSD disks; Model Checking
n3:klicoveSlovo
n15:SSD%20disks n15:Flash%20memory n15:Model%20Checking
n3:kontrolniKodProRIV
[849F5CD0496D]
n3:mistoKonaniAkce
L'Aquila, Italy
n3:mistoVydani
Neuveden
n3:nazevZdroje
Formal Methods for Industrial Critical Systems
n3:obor
n20:IN
n3:pocetDomacichTvurcuVysledku
3
n3:pocetTvurcuVysledku
5
n3:projekt
n8:1ET408050503 n8:GA201%2F06%2F1338
n3:rokUplatneniVysledku
n5:2009
n3:tvurceVysledku
Barnat, Jiří Šimeček, Pavel Edelkamp, Stefan Sulewski, Damian Brim, Luboš
n3:typAkce
n21:CST
n3:wos
000270704100010
n3:zahajeniAkce
2008-01-01+01:00
n3:zamer
n10:MSM0021622419
s:issn
0302-9743
s:numberOfPages
16
n12:doi
10.1007/978-3-642-03240-0_14
n23:hasPublisher
Springer-Verlag. (Berlin; Heidelberg)
n18:isbn
9783642032394
n22:organizacniJednotka
14330