The project addresses the problem of verifying software in C with respect to userdefined properties in the context of bounded model checking. Serving this goal, stateoftheart 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 based on successful verification of the old verification runs and reuse of the invested effort in consecutive verification runs.
We propose to reuse the function summaries extracted from Craig interpolation after a successful verification run. Function summaries are computed as overapproximations using Craig interpolation, a wellknown mechanism, useful to preserve the most relevant information of the function bodies. The function calls are then to be substituted by these overapproximations, and it leads to a more efficient and fast verification process.
There are two main tracks made within the project:
There are two approaches for extracting and reusing interpolationbased function summaries:

FunFrog: SATbased bounded model checker of a single C program using interpolationbased function summarization.

HiFrog: SMTbased bounded model checker of a single C program using SMTbased function summarization and Theory Refinement.
FunFrog focuses only on propositional logic and consequently, despite behaving in an incremental manner, FunFrog is expensive in many cases in practice. HiFrog considers the rich field of firstorder theories available in modern SMT solvers. On top of HiFrog we propose to use function summaries more generally by translating them to various SMT theories. Note that HiFrog significantly outperforms FunFrog.
2) Verification of different revisions of a program w.r.t a fixed property: Overapproximating function summaries are extracted after a successful verification run of one program version with a fixed property and reused while verifying other versions of the program w.r.t a fixed property.

eVolCheck: SATbased bounded upgrade checker of C program versions using interpolationbased function summarization.

UpProver: SMTbased incremental bounded model checker for verifying different revisions of a C program using SMTbased function summarization.
SATbased eVolCheck uses propositional encoding for modelinmg C programs, thus despite behaving in an incremental manner, it is expensive in many cases in practice due to bitblasting. UpProver in contrast to its predecessor, exploits firstorder theories available in SMT solvers, offering two more levels of encoding precision: linear arithmetic and uninterpreted functions, thus allowing a tradeoff between precision and performance. Note that UpProver significantly outperforms eVolCheck.