Wed 15 Jun 2016 10:30 - 11:00 at Grand Ballroom San Rafael - Verification I Chair(s): Isil Dillig

We present a new approach to inferring likely preconditions for black-box code. Like prior data-driven approaches, our approach employs a form of machine learning to infer a precondition that is consistent with a set of test executions. However, prior approaches require 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 in the black-box setting, we also show how to use PIE as the basis for a novel and general algorithm for inferring loop invariants when the code is available and analyzable by an automatic constraint solver. We demonstrate the capabilities of PIE by using it to infer rich preconditions for black-box OCaml library functions as well as verified loop invariants for C++ programs.