eVolCheck is a bounded upgrade checker of C, built on the top of FunFrog. It uses interpolation-based function summaries, extracted from the original version of a program, for incremental verification of an upgraded version of the program.
In each incremental check, eVolCheck first identifies the modified function on the syntactical level and then attempts to show that the old function summaries are still valid over-approximations of the behavior of the modified functions. These are local and thus cheap checks.
eVolCheck is integrated into the Verification-Aided Regression Testing (VART) framework, a novel extension of regression testing that uses model checking to increase the fault revealing capability of existing test suites. The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by (i) automatically producing assertions that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers’ intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counter-examples that are not revealed by the regression tests.
- Incremental Upgrade Checking by Means of Interpolation-based Function Summaries, , 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Cambridge, UK (2012)
- eVolCheck: Incremental Upgrade Checker for C, , 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rome, Italy (2013)
- Flexible SAT-based framework for incremental bounded upgrade checking, , TACAS (2013)
- Verification-Aided Regression Testing, , International Symposium on Software Testing and Analysis, San Jose, USA (2014)