  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.
