Formal verification of software changes and upgrades

The project addresses the problem of checking of software upgrades. Serving this goal, state-of-the-art model checkers hardly use the information of the old version, and reduce it thereby to the standalone verification. The purpose of the research is to develop a new technique for checking the software upgrades based on successful verification of the old program and reuse of the invested effort. 

We propose to reuse the function summaries, extracted from the old program in the upgraded version to prevent re-verification of the entire code. The method is based on the following observation. There are two possibilities for the modifed functions, either their old summaries are still a valid over-approximation or not. If they are valid, properties of the old version, for which the summaries are relevant, still hold also in the new version.

This idea has roots in our optimization of bounded model checking, which also allows reusing the interpolant-based function summaries for the verification runs for checking different properties of the same software. Function summaries are computed as over-approximations using Craig interpolation, a well-known mechanism, useful to preserve the most relevant information of the function bodies. The function calls are then to be substituted by these over-approximations, and it leads to a more efficient and fast verification process.

 - description of interpolation-based BMC: [1]

 - description of implementation in a tool FunFrog

 - description of interpolation-based upgrade checker: [2]

The project is partially supported by the PINCETTE EU FP7 STREP Project.

References