Data-Driven Precondition Inference with Learned Features
Data-Driven Precondition Inference with Learned Features
复制标题
DOI：
10.1145/2908080.2908099
复制
发表时间：
2016-06-01
影响因子：
--
通讯作者：
Millstein, Todd
中科院分区：
文献类型：
--
作者：
Padhi, Saswat;Sharma, Rahul;Millstein, Todd
我们将数据驱动的方法扩展到从一组测试执行中推断代码的先决条件。先前的工作需要一组固定的功能，即定义可能预先解决的搜索空间的原子谓词，并要预先指定。相比之下，我们引入了一项针对OnDemand特征学习的技术，该技术会根据需要以目标方式自动扩展候选先决条件的搜索空间。我们已经用称为pie的工具实例化了我们的方法。除了使前提推论更具表现力外，我们还展示了如何将我们的特征学习技术应用于数据驱动的循环不变推理的设置。我们通过使用PIE来评估我们的方法，以推断出Black-Box OCAML库功能的丰富先决条件，并使用我们的循环不变推理算法作为C ++程序的自动程序验证程序的一部分。
We extend the data-driven approach to inferring preconditions for code from a set of test executions. Prior work requires 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 ondemand 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, we show how to apply our featurelearning technique to the setting of data-driven loop invariant inference. We evaluate our approach by using PIE to infer rich preconditions for black-box OCaml library functions and using our loop-invariant inference algorithm as part of an automatic program verifier for C++ programs.