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
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-7714, INRIA. 2011, pp.32
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00615623
Contributeur : Claude Marché <>
Soumis le : vendredi 19 août 2011 - 17:43:10
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : lundi 12 novembre 2012 - 15:36:41

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00615623, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

475

Téléchargements de fichiers

411