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”

Incremental Upgrade Checking by Means of Interpolation-based Function Summaries

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10124357" target="_blank" >RIV/00216208:11320/12:10124357 - isvavai.cz</a>

  • Result on the web

    <a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462563" target="_blank" >http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462563</a>

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Incremental Upgrade Checking by Means of Interpolation-based Function Summaries

  • Original language description

    During its evolution, a typical software/hardware design undergoes a myriad of small changes. However, it is extremely costly to verify each new version from scratch. As a remedy to this problem, we propose to use function summaries to enable incrementalverification of the evolving systems. During the evolution, our approach maintains function summaries derived using Craig's interpolation. For each new version, these summaries are used to perform a local incremental check. Benefit of this approach is that the cost of the check depends on the extent of the change between the two versions and can be performed cheaply for incremental changes without resorting to re-verification of the entire system. Our implementation and experimentation in the context of the bounded model checking for C confirms that incremental changes can be verified efficiently for different classes of industrial programs.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    JC - Computer hardware and software

  • OECD FORD branch

Result continuities

  • Project

  • Continuities

    I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Others

  • Publication year

    2012

  • 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 in Computer-Aided Design (FMCAD '12)

  • ISBN

    978-1-4673-4832-4

  • ISSN

  • e-ISSN

  • Number of pages

    8

  • Pages from-to

    114-121

  • Publisher name

    IEEE

  • Place of publication

    Neuveden

  • Event location

    Cambridge, United Kingdom

  • Event date

    Oct 22, 2012

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article