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 JunDisplayed 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 30mTalk | 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 30mTalk | Cartesian Hoare Logic for Verifying k-Safety Properties Research Papers Media Attached | ||
11:30 30mTalk | Verifying Bit Manipulations of Floating-Point Research Papers Media Attached |