Learning Invariants using Decision Trees
Learning Invariants using Decision Trees
复制标题
使用决策树学习不变量
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
Siddharth Krishna;Christian Puhrsch;Thomas Wies
推断用于验证程序安全性的归纳不变量的问题可以用二元分类来表述。这是机器学习中的一个标准问题：给定一个好点和坏点的样本，要求找到一个分类器，该分类器从样本中概括并分离两个集合。这里，好的点是程序的可达状态，坏的点是那些违反安全属性的状态。因此，学习的分类器是候选不变量。在本文中，我们提出了一个新的算法，使用决策树学习候选不变量的形式的任意布尔组合的数值不等式。我们已经用我们的算法来验证从文献中提取的C程序。该算法是能够推断出安全的不变量的一系列具有挑战性的基准和媲美其他ML为基础的不变推理技术。特别是，它可以很好地扩展到大样本集。
The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other ML-based invariant inference techniques. In particular, it scales well to large sample sets.
反例引导焦点
DOI：
10.1145/1706299.1706330
发表时间：
2010
期刊：
影响因子：
--
作者：
A. Podelski;T. Wies
通讯作者：
T. Wies