Automatic Inference of Necessary Preconditions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Automatic Inference of Necessary Preconditions

Résumé

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%.

Domaines

Autre [cs.OH]

Dates et versions

hal-00930070 , version 1 (14-01-2014)

Identifiants

Citer

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⟩
174 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More