Interval counterexamples for loop invariant learning
Interval counterexamples for loop invariant learning
复制标题
循环不变学习的区间反例
DOI：
10.1145/3368089.3409752
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Bow
中科院分区：
文献类型：
--
作者：
Rongchen Xu;Fei He;Bow
循环不变式的生成一直是一个具有挑战性的问题。黑盒学习最近成为推断循环不变量的一种很有前途的方法。然而，性能在很大程度上取决于所收集样本的质量。在许多情况下，只有经过数十甚至数百个约束查询后，才能成功地推断出可行的不变量。为了减少大量的约束查询和提高黑盒学习的性能，我们在学习框架中引入了区间反例。每个区间反例表示约束解算器的一组反例。我们提出了三种不同的泛化技术来计算区间反例。对现有的决策树算法进行了改进，使其适应区间反例。我们评估了我们的技术，并报告在学习回合和验证时间上比最先进的方法提高了40%以上。
Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred. To reduce the gigantic number of constraint queries and improve the performance of black-box learning, we introduce interval counterexamples into the learning framework. Each interval counterexample represents a set of counterexamples from constraint solvers. We propose three different generalization techniques to compute interval counterexamples. The existing decision tree algorithm is also improved to adapt interval counterexamples. We evaluate our techniques and report over 40% improvement on learning rounds and verification time over the state-of-the-art approach.