2021年
Decision Tree Learning in CEGIS-Based Termination Analysis
Computer Aided Verification
- ,
- ,
- 開始ページ
- 75
- 終了ページ
- 98
- 記述言語
- 掲載種別
- 論文集(書籍)内論文
- DOI
- 10.1007/978-3-030-81688-9_4
- 出版者・発行元
- Springer International Publishing
<title>Abstract</title>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 <italic>cycles</italic> 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.
- リンク情報
- ID情報
-
- DOI : 10.1007/978-3-030-81688-9_4
- ISSN : 0302-9743
- eISSN : 1611-3349
- DBLP ID : conf/cav/KuraUH20