論文

査読有り
2021年

Decision Tree Learning in CEGIS-Based Termination Analysis

Computer Aided Verification
  • Satoshi Kura
  • ,
  • Hiroshi Unno
  • ,
  • Ichiro Hasuo

開始ページ
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.

リンク情報
DOI
https://doi.org/10.1007/978-3-030-81688-9_4
DBLP
https://dblp.uni-trier.de/rec/conf/cav/KuraUH20
URL
https://link.springer.com/content/pdf/10.1007/978-3-030-81688-9_4
ID情報
  • DOI : 10.1007/978-3-030-81688-9_4
  • ISSN : 0302-9743
  • eISSN : 1611-3349
  • DBLP ID : conf/cav/KuraUH20

エクスポート
BibTeX RIS