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”

Quo Vadis Explicit-State Model Checking

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F15%3A00082654" target="_blank" >RIV/00216224:14330/15:00082654 - isvavai.cz</a>

  • Result on the web

    <a href="http://dx.doi.org/10.1007/978-3-662-46078-8_5" target="_blank" >http://dx.doi.org/10.1007/978-3-662-46078-8_5</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-662-46078-8_5" target="_blank" >10.1007/978-3-662-46078-8_5</a>

Alternative languages

  • Result language

    angličtina

  • Original language name

    Quo Vadis Explicit-State Model Checking

  • Original language description

    Model checking has always been the flag ship in the fleet of automated formal verification techniques. It has been in the center of interest of formal verification research community for more than 25 years. Focusing primarily on the well-known state space explosion problem, a decent amount of techniques and methods have been discovered and applied to push further the frontier of systems verifiable with a model checker. Still, the technique as such has not yet been matured enough to become a common partof a software development process, and its penetration into the software industry is actually much slower than it was expected. In this paper we take a closer look at the so called explicit-state model checking, we briefly recapitulate recent research achievements in the field, and report on practical experience obtained from using our explicit state model checker DIVINE.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    IN - Informatics

  • OECD FORD branch

Result continuities

  • Project

    <a href="/en/project/7H13001" target="_blank" >7H13001: Critical System Engineering Acceleration</a><br>

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Others

  • Publication year

    2015

  • 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

    SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science

  • ISBN

    9783662460771

  • ISSN

    0302-9743

  • e-ISSN

  • Number of pages

    12

  • Pages from-to

    46-57

  • Publisher name

    Springer

  • Place of publication

    Neuveden

  • Event location

    Pec pod Sněžkou

  • Event date

    Jan 1, 2015

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article