Automatic inference of necessary preconditions

Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings
PublisherSpringer Verlag
Pages128-148
Number of pages21
ISBN (Print)9783642358722
DOIs
StatePublished - 2013
Event14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013 - Rome, Italy
Duration: Jan 20 2013Jan 22 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7737 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013
CountryItaly
CityRome
Period1/20/131/22/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automatic inference of necessary preconditions'. Together they form a unique fingerprint.

Cite this