Patrick Cousot, Radhia Cousot, Manuel Fähndrich, & Francesco Logozzo, Automatic Inference of Necessary Preconditions

Patrick Cousot, Radhia Cousot, Manuel Fähndrich, & Francesco Logozzo.
Automatic Inference of Necessary Preconditions
In Proceedings of the 14^th International Conference on Verification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni (Eds), Rome, Italy, January 21—22, 2013. Lecture Notes in Computer Science, Vol. 7737, pp. 128—148, © Springer 2013.
Paper:
- PDF (498 Kb)
Slides of the 25mn presentation at VMCAI'2013:
- 4 slides per landscape page, (160 Kb)
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%.
Keywords:
Abstract Interpretation, Clousot, Contracts, Design by contracts, Precondition, Static analysis.

Bibliographic reference:

\bibitem{CousotCousotFahndrichLLogozzo-VMCAI-13}
P.~Cousot, R.~Cousot, M.~F{\"a}hndrich, \& F.~Logozzo.
\newblock Automatic Inference of Necessary Preconditions.
\newblock In \emph{14th International Conference on Verification, Model Checking, 
          and Abstract Interpretation (VMCAI'13)}, Rome, Italy, 
          LNCS 7737, Springer, 2013, pp. 128--148.

@InProceedings{CousotCousotFahndrichLLogozzo-VMCAI-13,
 author    = {Patrick Cousot and
               Radhia Cousot and
               Manuel F{\"a}hndrich and
               Francesco Logozzo},
  title     = {Automatic Inference of Necessary Preconditions},
  pages     = {128--148},
  editor    = {Roberto Giacobazzi and
               Josh Berdine and
               Isabella Mastroeni},
  booktitle  = {Verification, Model Checking, and Abstract Interpretation,
               14th International Conference, VMCAI 2013, Rome, Italy,
               January 20--22, 2013. Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7737},
  year      = {2013},
}

copyright notice, Springer copyright notice
Last modified: Mon May 12 09:22:48 EDT 2014