Program verification is a challenging task that requires several techniques for addressing the different issues that arise from the complexity of the semantics of the underlying programming language. The program as well as the desired properties are expressed as logical formulas which when proved correct establishes the correctness of the program. The validity of such formulas are proven by deduction in a logical calculus. One main advantage of deductive verification is the ability to precisely model the semantics of the program. Frama-C is a platform that combines various program analysis and verification techniques for deductive verification of C programs. It operates on user-annotated C programs (in ACSL syntax) and generates verification conditions that would establish the correctness of input programs. These verification conditions are automatically discharged by a set of automated provers. The annotations provided by the user along with the program include function contracts, assertions, pre and post-conditions, loop invariants.
Among the annotations used, loop invariants are of special interest as writing a correct and useful loop invariant is as challenging as verifying the program itself. Thus the productivity of using Frama-C could be vastly improved by generating some of these loop invariants automatically. And this is the goal of our research endeavours. We propose techniques for generating these loop invariants. Our techniques are based on predicate abstraction - a well known abstract interpretation technique prevalent in abstract model-checking. We tune these techniques for our purposes and compute the abstractions at specific program points. The proposed techniques are implemented as Frama-C plugins. We also examined the potential of our technique on several tricky C programs as well as industrial benchmarks and the results are promising.