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.

翻译：我们提出一个数据驱动算法,用于数字变数合成和核实。算法基于ICE-DT的模型,用于从正反两种状态的样本中学习决策树,以及与程序过渡相应的影响。我们处理的主要问题是发现相关属性,用于数字变数的学习过程中。我们根据数据样本确定了解决这一问题的方法。它基于构建一个包含正反状态的分隔符,并排除与影响相符的负状态。分隔符是使用康韦克斯组合的抽象域域表示来构建的。决定树从分离器的限制中学习的通用机制使得一般变数的推论能够准确到能够证明目标属性。我们实施了我们的算法并展示了它的效率。