Modular inference of subprogram contracts for safety checking

Yannick Moy 1 Claude Marché 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2010, 45, pp.1184-1211
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00534331
Contributeur : Claude Marché <>
Soumis le : mercredi 10 novembre 2010 - 13:58:40
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 11 février 2011 - 02:37:49

Fichier

YJSCO1169.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00534331, version 1

Collections

Citation

Yannick Moy, Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, Elsevier, 2010, 45, pp.1184-1211. 〈inria-00534331〉

Partager

Métriques

Consultations de la notice

476

Téléchargements de fichiers

335