Automated Generation of Loop Invariants using Predicate Abstraction

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.La vérification de programmes est une tâche difficile qui nécessite plusieurs techniques pour traiter les différentes questions qui se posent en raison de la syntaxe du programme, la sémantique et dans de nombreux cas, le type de propriétés qui doivent être établies. L'analyse statique est l'une des techniques qui a obtenu quelques succès dans la vérification de logiciels de nature industrielle. Cependant, aucune technique n'est suffisante pour combattre la complexité des systèmes logiciels d'aujourd'hui. Une combinaison de techniques est la seule façon d'avancer en vue d'atteindre les niveaux de confiance qui sont nécessaires en matière de sécurité des logiciels critiques. Frama-C est un exemple de plate-forme qui combine plusieurs techniques d'analyse et de vérification. Elle se compose d'un ensemble d'outils qui fonctionnent sur des programmes C annotés et génère des conditions de vérification qui établissent la correction des programmes fournis. Ces conditions de vérification sont automatiquement validées par un ensemble de prouveurs automatiques. Les annotations fournies par l'utilisateur avec le programme comprennent les contrats de fonction, les assertions et les invariants de boucle. Parmi ces annotations, les invariants de boucle sont les plus ardus à déterminer car le bon choix d'un invariant correct et utile est aussi difficile que de vérifier le programme lui-même. Dans cet article, nous décrivons les techniques que nous avons développé pour générer ces invariants de boucles automatiquement pour réduire la tâche de l'utilisateur. Nos techniques sont basées sur l'abstraction booléenne (Predicate Abstraction en anglais), une technique bien connue dans le cadre de l'interprétation abstraite et du Model-Checking. Nous démontrons le potentiel de notre technique par une mis en œuvre dans l'environnement Frama-C