Automated Generation of Loop Invariants using Predicate Abstraction

Krishnamani Kalyanasundaram 1, 2 Claude Marché 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Document type :
Reports
[Research Report] RR-7714, INRIA. 2011, pp.32
Liste complète des métadonnées

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/inria-00615623
Contributor : Claude Marché <>
Submitted on : Friday, August 19, 2011 - 5:43:10 PM
Last modification on : Thursday, February 9, 2017 - 3:56:17 PM
Document(s) archivé(s) le : Monday, November 12, 2012 - 3:36:41 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00615623, version 1

Citation

Krishnamani Kalyanasundaram, Claude Marché. Automated Generation of Loop Invariants using Predicate Abstraction. [Research Report] RR-7714, INRIA. 2011, pp.32. 〈inria-00615623〉

Share

Metrics

Record views

422

Files downloads

365