Decision Tree Learning in CEGIS-Based Termination Analysis

TL;DR

This paper introduces a decision tree-based algorithm integrated into CEGIS for synthesizing ranking functions to verify program termination, demonstrating promising results on benchmark problems.

Contribution

It presents a novel decision tree synthesis method within CEGIS that detects cycles for refining decision trees in termination analysis.

Findings

Effective on benchmark termination problems

Detects cycles for improved synthesis

Promising experimental results

Abstract

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.