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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

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