eVolCheck: Incremental Upgrade Checker for C

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F13%3A10193385" target="_blank" >RIV/00216208:11320/13:10193385 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-36742-7_21" target="_blank" >http://dx.doi.org/10.1007/978-3-642-36742-7_21</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-36742-7_21" target="_blank" >10.1007/978-3-642-36742-7_21</a>

Result language
angličtina
Original language name
eVolCheck: Incremental Upgrade Checker for C
Original language description
Software is not created at once. Rather, it grows incrementally version by version and evolves long after being first released. To be practical for software developers, the software verification tools should be able to cope with changes. In this paper, we present a tool, eVolCheck, that focuses on incremental verification of software as it evolves. During the software evolution the tool maintains abstractions of program functions, function summaries, derived using Craig interpolation. In each check, thefunction summaries are used to localize verification of an upgrade to analysis of the modified functions. Experimental evaluation on a range of various benchmarks shows substantial speedup of incremental upgrade checking of eVolCheck in contrast to checking each version from scratch.
Czech name
—
Czech description
—

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

Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-642-36741-0
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
292-307
Publisher name
Springer Berlin Heidelberg
Place of publication
Berlin, Germany
Event location
Italy
Event date
Mar 16, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)