Automated Generation of Loop Invariants using Predicate Abstraction
Krishnamani Kalyanasundaram, Claude Marché · HAL (Le Centre pour la Communication Scientifique Directe) · 2011
Program verification is a challenging task that requires several techniques for addressing the different issues that arise because of program syntax, semantics and in many cases, the kind of properties that are to be established. Static analysis is one of the techniques that has anchored its presence in the verification of industrial scale softwares. However, no one technique is enough to combat the complexity of today's software systems. A combination of techniques is the only way forward in order to achieve the confidence levels that are required in safety-critical softwares. Frama-C is one such platform that combines various program analyses and verification techniques. It consists of a bunch of tools that operate on user-annotated C programs and generates verification conditions that would establish the correctness of the 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 and loop invariants. Of these annotations, loop invariants are of special interest as writing a correct and useful loop invariant is as challenging as verifying the program itself. In this article, we describe the techniques we have developed for generating these loop invariants automatically to reduce the burden on the user. Our techniques are based on Predicate Abstraction, a well known abstract interpretation technique for abstract model-checking. We demonstrate the potential of our technique in a multi-prover verification of C-programs as implemented in Frama-C platform.