论文标题
数据驱动的数值不变综合，具有自动生成的属性
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
论文作者
论文摘要
我们提出了一种数据驱动的算法，用于数值不变综合和验证。该算法基于ICE-DT模式，用于从正状态和负面状态的样本中学习决策树以及与程序过渡相对应的含义。我们解决的主要问题是在数值不变符的学习过程中发现要使用的相关属性。我们定义了一种以数据样本为指导的解决此问题的方法。它基于覆盖积极状态并排除负面状态的分离器的构造，与含义一致。使用凸集的抽象域表示构建分离器。决策树从分离器的约束中学习的概括机制允许推断一般不变性，足以证明目标属性。我们实施了算法并显示了其效率。
We propose a data-driven algorithm for numerical invariant synthesis and verification. The algorithm is based on the ICE-DT schema for learning decision trees from samples of positive and negative states and implications corresponding to program transitions. The main issue we address is the discovery of relevant attributes to be used in the learning process of numerical invariants. We define a method for solving this problem guided by the data sample. It is based on the construction of a separator that covers positive states and excludes negative ones, consistent with the implications. The separator is constructed using an abstract domain representation of convex sets. The generalization mechanism of the decision tree learning from the constraints of the separator allows the inference of general invariants, accurate enough for proving the targeted property. We implemented our algorithm and showed its efficiency.
