Decision Tree Learning in CEGIS-Based Termination Analysis
Decision Tree Learning in CEGIS-Based Termination Analysis
复制标题
基于 CEGIS 的终止分析中的决策树学习
DOI：
10.1007/978-3-030-81688-9_4
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Hasuo Ichiro
中科院分区：
文献类型：
--
作者：
Kura Satoshi;Unno Hiroshi;Hasuo Ichiro
提出了一种新的基于决策树的排序函数综合算法，用于验证程序的可终止性。我们的算法集成到反例引导归纳合成（CEGIS）的工作流程。CEGIS是一个迭代学习模型，在每次迭代中，（1）合成器从当前示例中合成候选解决方案，（2）验证器接受候选解决方案，如果它是正确的，或者拒绝它，提供反例作为下一个示例的一部分。我们的主要新奇在于合成器的设计：在通常的决策树学习算法之上构建，我们的算法在一组示例转换中检测循环，并使用它们来细化决策树。我们已经实现了所提出的方法，并取得了可喜的实验结果，现有的基准集（非）终止验证问题，需要合成分段定义的字典仿射排名功能。
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detectscyclesin a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
European Symposium on Programming
影响因子：
--
作者：
Caterina Urban;A. Miné
通讯作者：
A. Miné
使用决策树学习不变量
DOI：
--
发表时间：
2015
期刊：
arXiv.org
影响因子：
--
作者：
Siddharth Krishna;Christian Puhrsch;Thomas Wies
通讯作者：
Thomas Wies
DOI：
--
发表时间：
2007
期刊：
International Conference on Rewriting Techniques and Applications
影响因子：
--
作者：
C. Marché;H. Zantema
通讯作者：
H. Zantema
DOI：
10.1145/2737924.2737976
发表时间：
2015
期刊：
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
L. Gonnord;D. Monniaux;Gabriel Radanne
通讯作者：
Gabriel Radanne
通过谓词约束可满足性模理论进行程序验证
DOI：
--
发表时间：
2020
期刊：
arXiv.org
影响因子：
--
作者：
Hiroshi Unno;Yuki Satake;Tachio Terauchi;Eric Koskinen
通讯作者：
Eric Koskinen