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
Volume7737 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Precondition
Necessary
Sufficient
Abstract Interpretation
Program Analysis

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., Cousot, R., Fähndrich, M., & Logozzo, F. (2013). Automatic inference of necessary preconditions. In Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings (Vol. 7737 LNCS, pp. 128-148). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7737 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-35873-9_10

Automatic inference of necessary preconditions. / Cousot, Patrick; Cousot, Radhia; Fähndrich, Manuel; Logozzo, Francesco.

Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Vol. 7737 LNCS Springer Verlag, 2013. p. 128-148 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7737 LNCS).

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

Cousot, P, Cousot, R, Fähndrich, M & Logozzo, F 2013, Automatic inference of necessary preconditions. in Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. vol. 7737 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7737 LNCS, Springer Verlag, pp. 128-148, 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, Rome, Italy, 1/20/13. https://doi.org/10.1007/978-3-642-35873-9_10
Cousot P, Cousot R, Fähndrich M, Logozzo F. Automatic inference of necessary preconditions. In Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Vol. 7737 LNCS. Springer Verlag. 2013. p. 128-148. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-35873-9_10
Cousot, Patrick ; Cousot, Radhia ; Fähndrich, Manuel ; Logozzo, Francesco. / Automatic inference of necessary preconditions. Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Vol. 7737 LNCS Springer Verlag, 2013. pp. 128-148 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ff34f993337749e1bcff5d7bcb99ce0f,
title = "Automatic inference of necessary preconditions",
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{\%}.",
author = "Patrick Cousot and Radhia Cousot and Manuel F{\"a}hndrich and Francesco Logozzo",
year = "2013",
doi = "10.1007/978-3-642-35873-9_10",
language = "English (US)",
isbn = "9783642358722",
volume = "7737 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "128--148",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings",

}

TY - GEN

T1 - Automatic inference of necessary preconditions

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Fähndrich, Manuel

AU - Logozzo, Francesco

PY - 2013

Y1 - 2013

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

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

UR - http://www.scopus.com/inward/record.url?scp=84880104171&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84880104171&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-35873-9_10

DO - 10.1007/978-3-642-35873-9_10

M3 - Conference contribution

SN - 9783642358722

VL - 7737 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 128

EP - 148

BT - Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings

PB - Springer Verlag

ER -