Incremental Upgrade Checking by Means of Interpolation-based Function Summaries

Kód výsledku v 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>

Výsledek na webu

<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

—

Jazyk výsledku

angličtina

Název v původním jazyce

Incremental Upgrade Checking by Means of Interpolation-based Function Summaries

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Incremental Upgrade Checking by Means of Interpolation-based Function Summaries

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

Kód důvěrnosti údajů

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

Název statě ve sborníku

Formal Methods in Computer-Aided Design (FMCAD '12)

ISBN

978-1-4673-4832-4

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

114-121

Název nakladatele

IEEE

Místo vydání

Neuveden

Místo konání akce

Cambridge, United Kingdom

Datum konání akce

22. 10. 2012

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—