Data-Driven Precondition Inference with Learned Features

Saswat PadhiRahul SharmaTodd Millstein

⟬   Winner of SyGuS-Comp (Inv Track) 2017 – 18 ⟭  

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

  ACM DL
  PDF
  Tool
  Slides
  Talk
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.

BibTeX Citation
@inproceedings{pldi16/padhi/pie,
  title     = {Data-Driven Precondition Inference with Learned Features},
  author    = {Saswat Padhi and
               Rahul Sharma and
               Todd D. Millstein},
  booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation, {PLDI} 2016, Santa Barbara, CA,
               USA, June 13-17, 2016},
  pages     = {42--56},
  publisher = {ACM},
  year      = {2016},
  url       = {https://doi.org/10.1145/2908080.2908099},
  doi       = {10.1145/2908080.2908099}
}