The architecture is depicted on the following diagram:

eVolCheck works with goto-binaries, unwound up to the same fixed bound.

After verifying a software version, eVolCheck stores a set of function summaries, which are then used to speed up verification of an upgraded version. Initially, a bootstrapping run, roughly equivalent to the standalone verification done by FunFrog, is necessary to create the set of function summaries. 

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. If they succeed, the new version is safe. If not, the checks are propagated to the parent functions until either they succeed on some level of the call tree, or the check fails for the main function in the root of the call tree. In the former case, new valid summaries are generated for the subtree, while in the latter case, a real error is identified and reported to the user. As a result eVolCheck tends to exploit the locality of the changes, resulting in quick verification of upgrades that do not affect semantics of the code.