Data-Driven Precondition Inference with Learned Features

Saswat Padhi, Rahul Sharma, Todd Millstein

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016
(PLDI 2016)

  PDF
  Tool
  Video
  Slides

Abstract:
We extend the data-driven approach to inferring preconditions for code from a set of test executions. Prior work requires a fixed set of features, atomic predicates that define the search space of possible preconditions, to be specified in advance. In contrast, we introduce a technique for on-demand feature learning, which automatically expands the search space of candidate preconditions in a targeted manner as necessary. We have instantiated our approach in a tool called PIE. In addition to making precondition inference more expressive, we show how to apply our feature-learning technique to the setting of data-driven loop invariant inference. We evaluate our approach by using PIE to infer rich preconditions for black-box OCaml library functions and using our loop-invariant inference algorithm as part of an automatic program verifier for C++ programs.