基于CEGIS终止性分析的决策树学习
Decision Tree Learning in CEGIS-Based Termination Analysis
摘要：
提出了一种新的基于决策树的排序函数综合算法，用于验证程序的可终止性.我们的算法集成到反例引导归纳合成（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 detects cycles in 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
