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 implemented in the CProver framework (www.cprover.org). For satisfiability checks as well as for interpolant generation, eVolCheck uses PeRIPLO.

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.

Published papers: