All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

External Memory LTL 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%3A00047049" target="_blank" >RIV/00216224:14330/09:00047049 - isvavai.cz</a>

  • Result on the web

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    External Memory LTL Model Checking

  • Original language description

    Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated

  • Czech name

  • Czech description

Classification

  • Type

    O - Miscellaneous

  • CEP classification

    IN - Informatics

  • OECD FORD branch

Result continuities

  • Project

  • Continuities

    Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Others

  • Publication year

    2009

  • Confidentiality

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