eVolCheck

eVolCheck is a bounded upgrade checker of C, built on the top of FunFrog. It uses interpolation-based function summaries, extracted from 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 behaviour 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.

Sections:
Architecture
Download