Dynamic inference of likely data preconditions over predicates by tree learning

Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivaňić, Aarti Gupta

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

25 Scopus citations

Abstract

We present a technique to infer likely data preconditions for procedures written in an imperative programming language. Given a procedure and a set of predicates over its inputs, our technique enumerates different truth assignments to the predicates, deriving test cases from each feasible truth assignment. The predicates themselves are derived automatically using simple heuristics. The enumeration of truth assignments is performed using a propositional SAT solver along with a theory satisfiability checker capable of generating unsatisfiable cores. For each assignment of truth values, a corresponding set of test cases are generated and executed. Based on the result of the execution, the truth assignment is classified as being safe or buggy. Finally, a decision tree classifier is used to generate a Boolean formula over the input predicates that explains the data obtained from the test cases. The resulting Boolean formula is, in effect, a likely data precondition for the procedure under consideration. We apply our techniques on a wide variety of functions from the standard C library. Our experiments show that the proposed technique is quite robust. For most cases, it successfully learns a precondition that captures a safe and permissive calling environment.

Original languageEnglish (US)
Title of host publicationISSTA'08
Subtitle of host publicationProceedings of the 2008 International Symposium on Software Testing and Analysis 2008
Pages295-305
Number of pages11
DOIs
StatePublished - 2008
Externally publishedYes
Event2008 International Symposium on Software Testing and Analysis, ISSTA 2008 - Seattle, WA, United States
Duration: Jul 20 2008Jul 24 2008

Publication series

NameISSTA'08: Proceedings of the 2008 International Symposium on Software Testing and Analysis 2008

Other

Other2008 International Symposium on Software Testing and Analysis, ISSTA 2008
CountryUnited States
CitySeattle, WA
Period7/20/087/24/08

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Software

Keywords

  • Decision trees
  • Machine learning
  • SAT
  • Software specification
  • Verification

Fingerprint Dive into the research topics of 'Dynamic inference of likely data preconditions over predicates by tree learning'. Together they form a unique fingerprint.

  • Cite this

    Sankaranarayanan, S., Chaudhuri, S., Ivaňić, F., & Gupta, A. (2008). Dynamic inference of likely data preconditions over predicates by tree learning. In ISSTA'08: Proceedings of the 2008 International Symposium on Software Testing and Analysis 2008 (pp. 295-305). (ISSTA'08: Proceedings of the 2008 International Symposium on Software Testing and Analysis 2008). https://doi.org/10.1145/1390630.1390666