About: Can Flash Memory Help in Model Checking?     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
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. (en)
Title
  • Can Flash Memory Help in Model Checking?
  • Can Flash Memory Help in Model Checking? (en)
skos:prefLabel
  • Can Flash Memory Help in Model Checking?
  • Can Flash Memory Help in Model Checking? (en)
skos:notation
  • RIV/00216224:14330/09:00065776!RIV14-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(1ET408050503), P(GA201/06/1338), Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 305795
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/09:00065776
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Flash memory; SSD disks; Model Checking (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [849F5CD0496D]
http://linked.open...v/mistoKonaniAkce
  • L'Aquila, Italy
http://linked.open...i/riv/mistoVydani
  • Neuveden
http://linked.open...i/riv/nazevZdroje
  • Formal Methods for Industrial Critical Systems
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Barnat, Jiří
  • Brim, Luboš
  • Šimeček, Pavel
  • Edelkamp, Stefan
  • Sulewski, Damian
http://linked.open...vavai/riv/typAkce
http://linked.open...ain/vavai/riv/wos
  • 000270704100010
http://linked.open.../riv/zahajeniAkce
http://linked.open...n/vavai/riv/zamer
issn
  • 0302-9743
number of pages
http://bibframe.org/vocab/doi
  • 10.1007/978-3-642-03240-0_14
http://purl.org/ne...btex#hasPublisher
  • Springer-Verlag. (Berlin; Heidelberg)
https://schema.org/isbn
  • 9783642032394
http://localhost/t...ganizacniJednotka
  • 14330
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software