Deductive Verification with the Help of Abstract Interpretation

Abstract : Abstract interpretation is widely used in static analysis tools. However, to the best of our knowledge, it has not been extensively experimented in an interactive deductive verification context. This paper describes an analysis by abstract interpretation to infer loop invariants in the Why3 tool. The analysis takes advantage of the logic annotations present in the source code, including potential handwritten loop invariants. The inferred invariants are added to loops as if written by the user. They are checked by external provers and thus the analysis by abstract interpretation does not need to be trusted. Our analysis goes beyond numerical invariants. We describe two functors that add uninterpreted functions and quantifiers to a numerical abstract domain. The resulting domain is generic enough to reason about algebraic types, Booleans, or arrays. We show that it achieves a level of expressivity comparable to that of ad-hoc domains for arrays found in the literature.
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
Contributeur : Lucas Baudin <>
Soumis le : lundi 13 novembre 2017 - 23:44:43
Dernière modification le : mardi 24 avril 2018 - 17:20:12
Document(s) archivé(s) le : mercredi 14 février 2018 - 15:28:56


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01634318, version 1



Lucas Baudin. Deductive Verification with the Help of Abstract Interpretation. 2017. 〈hal-01634318〉



Consultations de la notice


Téléchargements de fichiers