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.

Wed 15 Jun

pldi-2016-papers
10:30 - 12:00: Research Papers - Verification I at Grand Ballroom San Rafael
Chair(s): Isil DilligUniversity of Texas, Austin
pldi-2016-papers146597940000010:30 - 11:00
Talk
Saswat PadhiUniversity of California, Los Angeles, Rahul SharmaStanford University, Todd MillsteinUniversity of California, Los Angeles
Media Attached
pldi-2016-papers146598120000011:00 - 11:30
Talk
Marcelo SousaUniversity of Oxford, Isil DilligUniversity of Texas, Austin
Media Attached
pldi-2016-papers146598300000011:30 - 12:00
Talk
Wonyeol Lee, Rahul SharmaStanford University, Alex AikenStanford University
Media Attached