Wed 15 Jun 2016 10:30 - 11:00 at Grand Ballroom San Rafael - Verification I Chair(s): Işıl 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

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Verification IResearch Papers at Grand Ballroom San Rafael
Chair(s): Işıl Dillig University of Texas, Austin
10:30
30m
Talk
Data-Driven Precondition Inference with Learned Features
Research Papers
Saswat Padhi University of California, Los Angeles, Rahul Sharma Stanford University, Todd Millstein University of California, Los Angeles
Media Attached
11:00
30m
Talk
Cartesian Hoare Logic for Verifying k-Safety Properties
Research Papers
Marcelo Sousa University of Oxford, Işıl Dillig University of Texas, Austin
Media Attached
11:30
30m
Talk
Verifying Bit Manipulations of Floating-Point
Research Papers
Wonyeol Lee Stanford University, Rahul Sharma Stanford University, Alex Aiken Stanford University
Media Attached