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
—