Automatic Inference of Necessary Preconditions

Patrick Cousot 1, 2, * Radhia Cousot 1, 3 Manuel Fähndrich 4 Francesco Logozzo 4
* Auteur correspondant
1 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : We consider the problem of automatic precondition inference. We argue that the common notion of sufficient precondition inference (i.e., under which precondition is the program correct?) imposes too large a burden on callers, and hence it is unfit for automatic program analysis. Therefore, we define the problem of necessary precondition inference (i.e., under which precondition, if violated, will the program always be incorrect?). We designed and implemented several new abstract interpretation-based analyses to infer atomic, disjunctive, universally and existentially quantified necessary preconditions. We experimentally validated the analyses on large scale industrial code. For unannotated code, the inference algorithms find necessary preconditions for almost 64% of methods which contained warnings. In 27% of these cases the inferred preconditions were also sufficient, meaning all warnings within the method body disappeared. For annotated code, the inference algorithms find necessary preconditions for over 68% of methods with warnings. In almost 50% of these cases the preconditions were also sufficient. Overall, the precision improvement obtained by precondition inference (counted as the additional number of methods with no warnings) ranged between 9% and 21%.
Type de document :
Communication dans un congrès
Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 - 14th Conference on Verification, Model Checking and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.128-148, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_10〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00930070
Contributeur : Jérôme Feret <>
Soumis le : mardi 14 janvier 2014 - 11:47:27
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

Collections

Citation

Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo. Automatic Inference of Necessary Preconditions. Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 - 14th Conference on Verification, Model Checking and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.128-148, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_10〉. 〈hal-00930070〉

Partager

Métriques

Consultations de la notice

199