Skip to Main content Skip to Navigation
Conference papers

Automatic Inference of Necessary Preconditions

Patrick Cousot 1, 2, * Radhia Cousot 1, 3 Manuel Fähndrich 4 Francesco Logozzo 4
* Corresponding author
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%.
Document type :
Conference papers
Complete list of metadatas
Contributor : Jérôme Feret <>
Submitted on : Tuesday, January 14, 2014 - 11:47:27 AM
Last modification on : Tuesday, September 22, 2020 - 3:46:01 AM

Links full text




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



Record views