The project addresses the problem of verifying software in C with respect to user-defined properties in the context of bounded model checking. 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 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 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.

There are two main tracks made within the project:

There are two approaches for extracting and reusing interpolation-based function summaries:

•  FunFrog: SAT-based bounded model checker of a single C program using interpolation-based function summarization.

•  HiFrog: SMT-based bounded model checker of a single C program using SMT-based 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 first-order 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: Over-approximating 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: SAT-based bounded upgrade checker of C program versions using interpolation-based function summarization.

• UpProver: SMT-based incremental bounded model checker for verifying different revisions of a C program using SMT-based function summarization.

SAT-based 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 bit-blasting. UpProver in contrast to its predecessor, exploits first-order theories available in SMT solvers, offering two more levels of encoding precision: linear arithmetic and uninterpreted functions, thus allowing a trade-off between precision and performance. Note that UpProver significantly outperforms eVolCheck.

Publications: