日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集

Decision Tree Learning in CEGIS-Based
Termination Analysis
Satoshi Kura

Hiroshi Unno

Ichiro Hasuo

We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workﬂow 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 asynthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a setof example transitions and uses them for reﬁning decision trees. We have implemented the proposed method
and obtained promising experimental results on existing benchmark sets of (non-)termination veriﬁcation
problems that require synthesis of piecewise-deﬁned lexicographic aﬃne ranking functions.

a candidate solution σ

1 Introduction
Termination Veriﬁcation by Ranking Functions and CEGIS
Termination veriﬁcation is a fundamental but
challenging problem in program analysis. Termination veriﬁcation usually involves some wellfoundedness arguments. Among them are thosemethods which synthesize ranking functions [16]:a ranking function assigns a natural number (or an
ordinal, more generally) to each program state, insuch a way that the assigned values strictly decrease
along transition. Existence of such a ranking function witnesses termination, where well-foundednessof the set of natural numbers (or ordinals) is crucially used.
We study synthesis of ranking functions by CounterExample Guided Inductive Synthesis (CEGIS) [28].
CEGIS is an iterative learning model in which a
synthesizer and a validator interact to ﬁnd solutions for given constraints. At each iteration, (1) asynthesizer tries to ﬁnd a candidate solution from内藏 理史 蓮尾 一郎, 総合研究大学院大学 & 国立情報学研
究所, The Graduate University for Advanced Studies(SOKENDAI) & National Institute of Informatics.
海野 広志, 筑波大学 & 理化学研究所 革新知能統合研究センター, University of Tsukuba & RIKEN AIP.

Synthesizer:
ﬁnd a candidate
solution σ that is
consistent with E
No solution

constraints C

Validator:
Is σ a solution for C?

No: a set E of examples(Validator adds new examples to E)

Yes: answer σ

Fig. 1: the CEGIS architecture
the current examples, and (2) a validator accepts
the candidate solution if it is correct, or rejects it
providing counterexamples. These counterexamples are then used as part of the next examples(Fig. 1).
CEGIS has been applied not only to program veriﬁcation tasks (synthesis of inductive invariants [17,18, 24, 25], that of ranking functions [19], etc.) but
also to constraint solving (for CHC [12, 14, 27, 35],
for pwCSP(T ) [29,30], etc.). The success of CEGIS
is attributed to the degree of freedom that synthesizers enjoy. In CEGIS, synthesizers receive a setof individual examples that synthesizers can use invarious creative and speculative manners (such asmachine learning). In contrast, in other methods
such as [5–8,23,26], synthesizers receive logical constraints that are much more binding.
Segmented Synthesis in CEGIS-Based Ter-

mination Analysis
The choice of a candidate space for candidate solutions σ is important in CEGIS. A candidate spaceshould be expressive: by limiting a candidate space,
the CEGIS architecture may miss a genuine solution. At the same time, complexity should be low:a larger candidate space tends to be more expensive
for synthesizers to handle.
This tradeoﬀ is also in the choice of the typeof examples: using an expressive example type, asmall number of examples can prune a large portion of the candidate space; however, ﬁnding such
expressive examples tends to be expensive.
In this paper, we use piecewise aﬃne functions as
our candidate space for ranking functions. Piecewise aﬃne functions 
are functions of the formea1 · xe + b1 xe ∈ L1



..
f (e
x) =
(1)
.



e
a ·x
e+b
x
e∈L
n

n

n

where {L1 , . . . , Ln } is a partition of the domain off (ex) such that each Li is a polyhedron (i.e. a conjunction of linear inequalities). We say segmented
synthesis to emphasize that our synthesis targets
are piecewise aﬃne functions with case distinction.
Piecewise aﬃne functions stand on a good balance
between expressiveness and complexity: the tasksof synthesizers and validators can be reduced tolinear programming (LP); at the same time, casedistinction allows them to model a variety of situations, especially where there are discontinuities in
the function values and/or derivatives.
We use transition examples as our example type(Table 1). Transition examples are pairs of program states that represent transitions; they aremuch cheaper to handle compared to trace examples (ﬁnite traces of executions until termination)used e.g. in [15, 32]. The current work is the ﬁrst
to pursue segmented synthesis of ranking functions
with transition examples; see Table 1.
Decision Tree Learning for CEGIS-Based
Termination Analysis: a Challenge
In this paper, we represent piecewise aﬃne functions (1) by the data structure of decision trees.
The data structure suits the CEGIS architecture(Fig. 1): iterative reﬁnement of candidate solutions can be naturally expressed by growing decision trees. The main challenge of this paper isthe design of an eﬀective synthesizer for decision

Table 1: ranking function synthesis by CEGIS
example type
trace
transition\
examplesexamplescandidate spaceaﬃne[15, 32][19]
ranking functions
piecewise aﬃneranking functions[15, 32]

e+
2
e−
4
e+
3

h1

e1

h1

e+
1

our method

e2

e−
5

e4
e3

h2

h2
h1
h1

+

f1 (e
x)
{e1 }

h2

+
{e+
1 , e2 }−−{e−
4 , e5 }

+
{e+
3 }

(a) For invariants

h2
f2 (e
x)
{e2 }

f3 (e
x)
{e3 }

(b) For ranking functions

Fig. 2: Decision tree learning
trees—such a synthesizer learns decision trees fromexamples.
In fact, decision tree learning in the CEGIS architecture has already been actively pursued, for thesynthesis of invariants as opposed to ranking functions [12,14,18,22,35]. It is therefore a natural idea
to adapt the decision tree learning algorithms used
there, from invariants to ranking functions. However, we ﬁnd that a naive adaptation of those algorithms for invariants does not suﬃce: they are goodat handling state examples that appear in CEGIS
for invariants; but they are not good at handlingtransition examples.
More speciﬁcally, when decision tree learning isapplied to invariant synthesis (Fig. 2a), examples
are given in the form of program states labeled
as positive or negative. Decision trees are thenbuilt by iteratively selecting the best halfspaces—
where “best” is in terms of some quality measures—
until each leaf contains examples with the same label. One common quality measure used here is an
information-theoretic notion of information gain.
We extend this from invariant synthesis to ranking function synthesis where examples are given bytransitions instead of states (Fig. 2b). In this case,a major challenge is to cope with examples thatcross a border of the current segmentation—such as
the transition e4 crossing the border h1 in Fig. 2b.
Our decision tree learning algorithm should handle such crossing examples, taking into account theconstraints imposed on the leaf labels aﬀected bythose examples (the aﬀected leaf labels are f1 (ex)
and f3 (ex) in the case of e4 ).
Our Algorithm:
Cycle-Based Decision
Tree Learning for Transition Examples
We use what we call the cycle detection theorem(Theorem 17) as a theoretical tool to handle suchcrossing examples. The theorem claims the following: if there is no piecewise aﬃne ranking function
with the current segmentation of the domain (suchas the one in Fig. 2b given by h1 and h2 ), thenthis must be caused by a certain type of cycle ofconstraints, which we call an implicit cycle.
In our decision tree learning algorithm, when we
do not ﬁnd a piecewise aﬃne ranking function withthe current segmentation, we ﬁnd an implicit cycle and reﬁne the segmentation to break the cycle.
Once all the implicit cycles are gone, the cycle detection theorem guarantees the existence of a candidate piecewise aﬃne ranking function with thesegmentation.
We integrate this decision tree learning algorithm
in the CEGIS architecture (Fig. 1) and use it asa synthesizer. Our implementation of this framework gives promising experimental results on existing benchmark sets.
Contribution
Our contribution is summarized as follows.
• We provide a decision tree-based synthesizer for ranking functions integrated into the
CEGIS architecture. Our synthesizer uses
transition examples to ﬁnd candidate piecewiseaﬃne ranking functions. A major challenge
here, namely handling constraints arising fromcrossing examples, is coped with by our theoretical observation of the cycle detection theorem.
• We implement our synthesizer for ranking
functions implemented in MuVal and report
the experience of using MuVal for termination and non-termination analysis. The experiment results show that MuVal’s performance is comparable to state-of-the-art termi-

nation analyzers [7, 10, 13, 21] from Termination Competition 2020, and that MuVal can
prove (non-)termination of some benchmarks
with which other analyzers struggle.
Organization.
Section 2 shows the overview of our method via
examples. Section 3 explains our target class of
predicate constraint satisfaction problems and how
to encode (non-)termination problem into such constraints. In Section 4, we review CEGIS architecture, and then explain simpliﬁcation of examples into positive/negative examples. Section 5
proposes our main contribution, our decision treebased ranking function synthesizer. Section 6shows our implementation and experimental results. Related work is discussed in Section 7, andwe conclude in Section 8.

2 Preview by Examples
We present a preview of our method using concrete examples. We start with an overview of thegeneral CEGIS architecture, after which we proceed to our main contribution, namely a decision
tree learning algorithm for transition examples.
2. 1 Termination Veriﬁcation by CEGISOur method follows the usual workﬂow of termination veriﬁcation by CEGIS. It works as follows:
given a program, we encode the termination problem into a constraint solving problem, and then use
the CEGIS architecture to solve the constraint solving problem.
Encoding the termination problem.
The ﬁrst step of our method is to encode the termination problem as the set C of constraints.
Example 1. As a running example, consider thefollowing C program.
while ( x != 0) {if ( x < 0) { x ++; } else { x - -; }}The termination problem is encoded as the following constraints.
x < 0 ∧ x′ = x + 1 =⇒ R(x, x′ )(2)¬(x < 0) ∧ x′ = x − 1 =⇒ R(x, x′ ).
(3)Here, R is a predicate variable representing a wellfounded relation, and term variables x, x′ are universally quantiﬁed implicitly.
The set C of constraints claims that the transition relation for the given program is subsumed bysynthesizer

validator
E =∅

(i)
(iii)
(v)

R(x, x′ ) = ⊥E = {R(1, 0)}R(x, x′ ) = x > x′ ∧ x ≥ 0
E = {R(1, 0), R(−2, −1)}′′R(x, x ) = |x| > |x | ∧ |x| ≥ 0

y ≥ 0?
≥(ii)<
f (x, y) = −yx − 1 ≥ 0?

(iv)
≥

<

(vi)

Fig. 3: An example of CEGIS iterations
a well-founded relation. So, verifying termination
is now rephrased as the existence of a solution for
C. Note that we omitted constraints for invariants
for simplicity in this example (see Sect. 3 for thefull encoding).
Constraint solving by CEGIS.
The next step is to solve C by CEGIS.
In the CEGIS architecture, a synthesizer and avalidator iteratively exchange a set E of examples
and a candidate solution R(x, x′ ) for C. At the moment, we present a rough sketch of CEGIS, leaving
the details of our implementation to Sect. 2. 2.
Example 2. Fig. 3 shows how the CEGIS architecture solves the set C of constraints shown in (2)and (3). Fig. 3 consists of three pairs of interactions(i)-(vi) between a synthesizer and a validator.
(i) The synthesizer takes E = ∅ as a set ofexamples and returns a candidate solution
R(x, x′ ) = ⊥ synthesized from E. In general,candidate solutions are required to satisfy all
constraints in E, but the requirement is vacuously true in this case.
(ii) The validator receives the candidate solution
and ﬁnds out that the candidate solution is
not a genuine solution. The validator ﬁnds
that the assignment x = 1, x′ = 0 is a counterexample for (3), and thus adds R(1, 0) to
E to prevent the same candidate solution in
the next iteration.
(iii) The synthesizer receives the updated set E ={R(1, 0)} of examples, ﬁnds a ranking function f (x) = x for E (i.e. for the transition
from x = 1 to x′ = 0), and returns a candidate solution R(x, x′ ) = x > x′ ∧ x ≥ 0.
(iv) The validator checks the candidate solution,ﬁnds a counterexample x = −2, x′ = −1 for(2), and adds R(−2, −1) to E.
(v) The synthesizer ﬁnds a ranking function
f (x) = |x| for E and returns R(x, x′ ) =f (x, y) = x − 1

f (x, y) = 1 − x

f (x, y) =x − 1 y ≥ 0 ∧ x − 1 ≥ 0
1−x y ≥0∧x−1<0


−y
y<0
Fig. 4: An example of a decision tree that represents a piecewise aﬃne ranking function f (x, y)|x| > |x′ | ∧ |x| ≥ 0 as a candidate solution.
Note that the synthesizer have to synthesize
a piecewise aﬃne function here, but details
are deferred to Sect. 2. 2.
(vi) The validator accepts the candidate solution
because it is a genuine solution for C.
2. 2 Handling Cycles in Decision Tree
Learning
We explain the importance of handling cycles
in our decision tree-based synthesizer of piecewiseaﬃne ranking functions.
In what follows, we deal with such decision trees
as shown in Fig. 4: their internal nodes have aﬃneinequalities (i.e. halfspaces); their leaves have aﬃnefunctions; and overall, such a decision tree expresses a piecewise aﬃne function (Fig. 4). When
we remove leaf labels from such a decision tree, thenwe obtain a template of piecewise functions wherecondition guards are given but function bodies arenot. We shall call the latter a segmentation.
Input and output of our synthesizer.
The input of our synthesizer is a set E of transition examples (e.g. E = {R(1, 0), R(−2, −1)}) as
explained in Sect. 2. 1. The output of our synthesizer is a well-founded relation R(ex, xe′ ) := f (e
x) >
′
f (e
x ) ∧ f (ex) ≥ 0 where x
e is a sequence of variables
and f (ex) is a piecewise aﬃne function, which isrepresented by a decision tree (Fig. 4). Therefore
our synthesizer aims at learning a suitable decisiontree.
Reﬁning segmentations and handling cy-

cles.
Roughly speaking, our synthesizer learns decision
trees in the following steps.
1. Generate a set H of halfspaces from the given
set E of examples. This H serves as the vocabulary for internal nodes. Set the initial segmentation to be the one-node tree (i.e. the trivial
segmentation).
2. Try to synthesize a piecewise aﬃne ranking function f for E with the current
segmentation—that is, try to ﬁnd suitable leaf
labels. If found, then use this f in a candidate well-founded relation R(ex, xe′ ) = f (e
x) >
′
f (e
x ) ∧ f (ex) ≥ 0.
3. Otherwise, reﬁne the current segmentation
with some halfspace in H, and go to Step 2.
The key step of our synthesizer is Step 3. We show
a few examples.
Example 3. Suppose we are given E ={R(1, 0), R(−2, −1)} as a set of examples. Our
synthesizer proceeds as follows: (1) Our synthesizer generates the set H := {x ≥ 1, x ≥ 0, x ≥−2, x ≥ −1} from the examples in E. (2) Our
synthesizer tries to ﬁnd a ranking function of theform f (x) = ax + b (with the trivial segmentation),but there is no such ranking function. (3) Our
synthesizer reﬁnes the current segmentation with(x ≥ 0) ∈ H because x ≥ 0 “looks good”. (4) Our
synthesizer tries to ﬁnd a ranking function of theform f (x) = if x ≥ 0 then ax + b else cx + d, using
the current segmentation. Our synthesizer obtains
f (x) = if x ≥ 0 then x else − x and use this f (x)for a candidate solution.
How can we decide which halfspace in H “looks
good”? We use quality measure that is a value representing the quality of each halfspace and selectthe halfspace with the maximum quality measure.
Fig. 5 shows the comparison of the quality ofx ≥ 0 and x ≥ −2 in this example. Intuitively,x ≥ 0 is better than x ≥ −2 because we can obtaina simple ranking function if x ≥ 0 then x else − xwith x ≥ 0 (Fig. 5a) while we need further reﬁnement of the segmentation with x ≥ −2 (Fig. 5b).
In Sect. 5, we introduce a quality measure for halfspaces following this intuition.
Our synthesizer iteratively reﬁnes segmentations
following this quality measure, until examples contained in each leaf of the decision tree admit anaﬃne ranking function. This approach is inspired

f (x)
−2

−1

0

1

2

(a) Good (x ≥ 0)

−2

−1

0

1

2

(b) Bad (x ≥ −2)

Fig. 5: Selecting halfspaces. Transition examples
are shown by red arrows. Boundaries of halfspaces
are shown by dashed lines.

−2
−1
0
1
2
3
Fig. 6: Two examples R(−1, 1) and R(1, 0) makean implicit cycle between x ≥ 1 and ¬(x ≥ 1).
by the use of information gain in the decision tree
learning for invariant synthesis.
Example 3 showed a natural extension of a decision tree learning method for invariant synthesis.
However, this is not enough for transition examples, for the reasons of explicit and implicit cycles.
Here are their examples.
Example 4. Suppose we are given E ={R(1, 0), R(0, 1)}. In this case, there is no ranking function because E contains a cycle 1 → 0 → 1
witnessing non-termination. We call such a cycle
an explicit cycle.
Example 5. Let E= {R(−1, 1), R(1, 0),R(−1, −2), R(2, 3)} (Fig. 6). Our synthesizer proceeds as follows. (1) Our synthesizer generates theset H := {x ≥ 1, x ≥ 0, . . . } of halfspaces. (2)Our synthesizer tries to ﬁnd a ranking function of
the form f (x) = ax + b (with the trivial segmentation), but there is no such. (3) Our synthesizer
reﬁnes the current segmentation with (x ≥ 1) ∈ H
because x ≥ 1 “looks good” (i.e. is the best withrespect to a quality measure).
We have reached the point where the naive extension of decision tree learning explained in Example 3 no longer works: although all constraints
contained in each leaf of the decision tree admit anaﬃne ranking function, there is no piecewise aﬃneranking function for E of the form f (x) = if x ≥1 then ax + b else cx + d.
More speciﬁcally, in this example, the leaf representing x ≥ 1 contains R(2, 3), and the other leaf
representing ¬(x ≥ 1) contains R(−1, −2). The
example R(2, 3) admits an aﬃne ranking function
f1 (x) = −x + 2, and R(−1, −2) admits f2 (x) =x + 1, respectively. However, the combinationf (x) = if x ≥ 1 then f1 (x) else f2 (x) is nota ranking function for E. Moreover, there is noranking function for E of the form f (x) = if x ≥1 then ax + b else cx + d.
It is clear that this failure is caused by the crossing examples R(−1, 1) and R(1, 0). It is not thatevery crossing example is harmful. However, in thiscase, the set {R(−1, 1), R(1, 0)} forms a cycle between the leaf for x ≥ 1 and the leaf for ¬(x ≥ 1)(see Fig. 6). This “cycle” among leaves—in contrast to explicit cycles such as {R(1, 0), R(0, 1)} in
Example 4—is called an implicit cycle.
Once an implicit cycle is found, our synthesizer
cuts it by reﬁning the current segmentation. Our
synthesizer continues the above steps (1–3) of decision tree learning as follows. (4) Our synthesizer
selects (x ≥ 0) ∈ H and cuts the implicit cycle{R(−1, 1), R(1, 0)} by reﬁning segmentations. (5)Using the reﬁned segmentation, our synthesizer obtains f (x) = if x ≥ 1 then − x + 2 else if x ≥0 then 0 else x + 3 as a ranking function for E.
As explained in Example 4,5, handling (explicit
and implicit) cycles is crucial in decision tree learning for transition examples. Moreover, our cycle
detection theorem (Theorem 17) claims that if there
is no explicit or implicit cycle, then one can ﬁnd aranking function for E without further reﬁnementof segmentations.

3 (Non-)Termination Veriﬁcation as
Constraint Solving
We explain how to encode (non-)termination veriﬁcation to constraint solving.
Following [30], we formalize our target class
pwCSP of predicate constraint satisfaction problems parametrized by a ﬁrst-order theory T .
Deﬁnition 6. Given a formula ϕ, let ftv (ϕ) be theset of free term variables and fpv (ϕ) be the set offree predicate variables in ϕ.
Deﬁnition 7. A pwCSP is deﬁned as a pair (C, R)

where C is a ﬁnite set !
of clauses of the form
!
ℓ
m
_
_
e
e
ϕ∨
Xi (ti ) ∨¬Xi (ti )
i=1

i=ℓ+1

(4)

and R ⊆ fpv (C) is a set of predicate variables thatare required to denote well-founded relations. Here,0 ≤ ℓ ≤ m. Meta-variables t and ϕ range overT -terms and T -formulas, respectively, such thatftv (ϕ) = ∅. Meta-variables x and X range overterm and predicate variables, respectively.
A pwCSP (C, R) is called CHCs (constrainedHorn clauses, [9]) if R = ∅ and ℓ ≤ 1 for all clausesc ∈ C. The class of CHCs has been widely studied
in the veriﬁcation community [12, 14, 27, 35].
Deﬁnition 8. A predicate substitution σ is a ﬁnite
map from predicate variables X to closed predicatesof the form λx1 , . . . , xar(X) .ϕ. We write dom(σ) for
the domain of σ and σ(C) for the application of σ
to C.
Deﬁnition 9. A predicate substitution σ is a (genuine) solution for (C, R) if (1) fpv (C) ⊆ dom(σ);V(2) |=
σ(C) holds; and (3) for all X ∈ R,
σ(X) represents a well-founded relation, that is,sort(σ(X)) = (es, se) → • for some sequence se ofsorts and there is no inﬁnite sequence ve1 , ve2 , . . .
of sequences vei of values of the sorts se such that|= ρ(X)(evi , vei+1 ) for all i ≥ 1.
Encoding termination.
Given a set of initial state ι(ex) and a transition relation τ (ex, xe′ ), the termination veriﬁcation
problem is expressed by the pwCSP (C, R) whereR = {R}, and C consists of the following clauses.
ι(ex) =⇒ I(e
x)
τ (e
x, x
e′ ) ∧ I(ex) =⇒ I(e
x′ )
′
′
τ (e
x, x
e ) ∧ I(ex) =⇒ R(ex, xe)We use ϕ =⇒ ψ as syntax sugar for ¬ϕ∨ψ, so thisis a pwCSP. The well-founded relation R assertsthat τ is terminating. We also consider an invariant I for τ to avoid synthesizing ranking functions
on unreachable program states.
Encoding non-termination.
We can also encode a problem of non-termination
veriﬁcation to pwCSP via recurrent sets [20]. For
simplicity, we explain the encoding for the case of
only one program variable x. We consider a recurrent set R satisfying the following conditions.
ι(x) =⇒ R(x)(5)
R(x) =⇒ ∃x′ .τ (x, x′ ) ∧ R(x′ )(6)
To remove ∃ from (6), we use the following con-

straint that is equivalent to (6).
R(x) =⇒ E(x, 0)(7)
E(x, x′ ) =⇒ τ (x, x′ ) ∧ R(x′ )∨ S(x′ , x′ − 1) ∧ E(x, x′ − 1)∨ S(x′ , x′ + 1) ∧ E(x, x′ + 1)
(8)
The intuition is as follows. Given x in the recurrent set R, the relation E(x, x′ ) searches for thevalue of ∃x′ in (6). The search starts from x′ = 0
in (7), and x′ is nondeterministically incremented
or decremented in (8). The well-founded relation S
asserts that the search ﬁnishes within ﬁnite steps.
As a result, we obtain a pwCSP for non-termination
deﬁned by (C, R) where R = {S} and C is given by(5), (7), and (the disjunctive normal form of) (8).
Example 10. Consider the following C program.
while ( x > 0) { x = -2 * x + 9; }The non-termination problem is encoded as the
pwCSP (C, R) where R = {S}, and C consists ofx > 0 =⇒ R(x)R(x) =⇒ E(x, 0)E(x, x′ ) =⇒ x′ = −2x + 9 ∧ R(x′ )∨ (S(x′ , x′ − 1) ∧ E(x, x′ − 1))∨ (S(x′ , x′ + 1) ∧ E(x, x′ + 1)).
The program is non-terminating when x = 3. Thisis witnessed by a solution σ for (C, R), which is
given by σ(R)(x) := x = 3, σ(E)(x, x′ ) := x =3 ∧ 0 ≤ x′ ∧ x′ ≤ 3, and σ(S)(x′ , x′′ ) := x′′ =x′ + 1 ∧ x′′ ≤ 3.

4 CounterExample-Guided Inductive
Synthesis (CEGIS)
We explain how CounterExample-Guided Inductive Synthesis [28] (CEGIS for short) works fora given pwCSP (C, R) following [30]. Then, we
add the extraction of positive/negative examples
to the CEGIS architecture, which enables our decision tree-based synthesizer to use a simpliﬁed formof examples.
CEGIS proceeds through the iterative interaction
between a synthesizer and a validator (Fig. 1), in
which they exchange examples and candidate solutions.
Deﬁnition 11. A formula ϕ is an example of C if
V
ftv (ϕ) = ∅ and C |= ϕ hold. Given a set E ofexamples of C, a predicate substitution σ is a candidate solution for (C, R) that is consistent with E
if σ is a solution for (E, R).

Synthesizer.
The input for a synthesizer is a set E of examples of C collected from previous CEGIS iterations.
The synthesizer tries to ﬁnd a candidate solution σconsistent with E instead of a genuine solution for(C, R). If the candidate solution σ is found, thenσ is passed to the validator. If E is unsatisﬁable,
then E witnesses unsatisﬁability of (C, R). Detailsof our synthesizer is described in Sect. 5.
Validator.
A validator checks whether the candidate solution σ from the synthesizer is a genuine solution of(C, R) by using SMT solvers. That is, satisﬁabilityVV
of |= ¬ σ(C) is checked. If |= ¬ σ(C) is not satisﬁable, then σ is a genuine solution of the original
pwCSP (C, R), so the validator accepts this. Otherwise, the validator adds new examples to the set
E of examples. Finally, the synthesizer is invokedagain with the updated set E of examples.
V
If |= ¬ σ(C) is satisﬁable, new examples areconstructed as follows. Using SMT solvers, the validator obtains an assignment θ to term variables
such that |= ¬θ(ψ) holds for some ψ ∈ σ(C). By(4), |= ¬θ(ψ) is a clause of the form |= ¬θ(ϕ) ∧


Vℓ
Vm
e
e
i=1 ¬σ(Xi )(θ(ti )) ∧i=ℓ+1 σ(Xi )(θ(ti )) . To
prevent this counterexample from being found in
the next CEGIS iteration again, the validator adds
the following example to E.
mℓ__ti )) ∨¬Xi (θ(eti ))(9)Xi (θ(ei=1i=ℓ+1The CEGIS architecture repeats this interaction
between the synthesizer and the validator until agenuine solution for (C, R) is found or E witnesses
unsatisﬁability of (C, R).
Extraction of positive/negative examples.
Examples obtained in the above explanation area bit complex to handle in our decision tree-based
synthesizer: each example in E is a disjunction (9)of literals, which may contain multiple predicate
variables.
To simplify the form of examples, we extract from+−E the sets EX
and EXof positive examples (i.e.,examples of the form X(ev )) and negative examples (i.e., examples of the form ¬X(ev )) for eachX ∈ fpv (E). This allows us to synthesize a predicate σ(X) for each predicate variable X ∈ fpv (E)+separately. For simplicity, we write ve ∈ EX
and
−
+
−
ve ∈ EX instead of X(ev ) ∈ EX and ¬X(ev ) ∈ EX.
The extraction is done as follows. We ﬁrst substi-

tute for each predicate variable application X(ev ) inE a boolean variable bX(ev) to obtain a SAT problem
SAT(E). Then, we use SAT solvers to obtain an
assignment η that is a solution for SAT(E). If a solution η exists, then we construct positive/negative
examples from η; otherwise, E is unsatisﬁable.
Deﬁnition 12. Let η be a solution for SAT(E).
For each predicate variable X ∈ fpv (E), we de+ﬁne the set EXof positive examples and the set+
EX of negative examples under the assignment η
+
−
:= {e
:= {e
by EX
v | η(bX(ev) ) = true} and EXv |η(bX(ev) ) = false}.
Note that some of predicate variable applications
X(ev ) may not be assigned true nor false because
they do not aﬀect the evaluation of SAT(E). Suchpredicate variable applications are discarded from
+
−
{(EX
, EX
)}X∈fpv (E) .
Our method uses the extraction of positive andnegative examples when the validator passes examples to the synthesizer. If X ∈ fpv (E) ∩ R, then we
−
+
).
, EX
apply our ranking function synthesizer to (EXIf X ∈ fpv (E) \ R, then we apply an invariant synthesizer.
We say a candidate solution σ is consistent+−
with {(EX, EX)}X∈fpv (E) if |= σ(X)(ev + ) and |=−¬σ(X)(ev ) hold for each predicate variable X ∈−+. If a candidate so, and ve− ∈ EX
fpv (E), ve+ ∈ EX−+)}X∈fpv (E) , thenlution σ is consistent with {(EX , EX
σ is also consistent with E.
+−
Note that unsatisﬁability of {(EX, EX)}X∈fpv (E)does not immediately implies unsatisﬁability of E+−
nor (C, R) because {(EX, EX)}X∈fpv (E) depends onthe choice of the assignment η. Therefore, the
CEGIS architecture need to be modiﬁed: if syn+−thesizers ﬁnd unsatisﬁability of {(EX, EX)}X∈fpv (E) ,then we add the negation of an unsatisﬁability core
to E to prevent using the same assignment η again.
Note that some restricted forms of (9) have also
been considered in previous work and are called implication examples in [17] and implication/negation
constraints in [12]. Our extraction of positive andnegative examples is applicable to the general formof (9).

5 Ranking Function Synthesis
In this section, we describe one of the main contributions, that is, our decision tree-based synthesizer, which synthesizes a candidate well-founded+
relation σ(R) from a ﬁnite set ER
of examples. We
assume that only positive examples are given because well-founded relations occur only positivelyin pwCSP for termination analysis (see Sect. 3).
The aim of our synthesizer is to ﬁnd a piecewiseaﬃne lexicographic ranking function fe(ex) for the+
given set ER of examples. Below, we ﬁx a predicate+
variable R ∈ R and omit the subscript ER= E +.

5. 1 Basic Deﬁnitions
To represent piecewise aﬃne lexicographic ranking functions, we use decision trees like the one in
Figure 4. Let xe = (x1 , . . . , xn ) be the program variables where each xi ranges over Z.
Deﬁnition 13. A decision tree D is deﬁned by
D := ge(ex) | if h(ex) ≥ 0 then D else D wherege(ex) = (gk (ex), . . . , g0 (ex)) is a tuple of aﬃne functions and h(ex) is an aﬃne function. A segmentation tree S is deﬁned as a decision tree with undeﬁned leaves ⊥: that is, S := ⊥ | if h(ex) ≥0 then S else S. For each decision tree D, we
can canonically assign a segmentation tree by replacing the label of each leaf with ⊥. This is denoted by S(D). For each decision tree D, we denote the corresponding piecewise aﬃne function by
feD (ex) : Zn → Zk+1 .
Each leaf in a segmentation tree S corresponds
to a polyhedron. We often identify the segmentation tree S with the set of leaves of S and a leaf
with the polyhedron corresponding to the leaf. For
example, we say something like “for each L ∈ S,
ve ∈ L is a point in the polyhedron L”.
Suppose we are given a segmentation tree S anda set E + of examples.
Deﬁnition 14. For each L1 , L2 ∈ S, we denotethe set of example transitions from L1 to L2 by
EL+1 ,L2 := {(ev , ve′ ) ∈ E + | ve ∈ L1 , ve′ ∈ L2 }.
An example (ev , ve′ ) ∈ E + is crossing w.r.t. S if+′(ev , ve ) ∈ EL1 ,L2 for some L1 ̸= L2 , and non-crossing+if (ev , ve′ ) ∈ EL,Lfor some L.
Deﬁnition 15. We deﬁne the dependency graph
G(S, E + ) for S and E + by the graph (V, E) wherevertices V = S are leaves, and edges E ={(L1 , L2 ) | L1 ̸= L2 , ∃(ev , ve′ ) ∈ EL+1 ,L2 } are crossing examples.
We denote the set of start points ve and end pointsve′ of examples (ev , ve′ ) ∈ E + by E + := {ev | (ev , ve′ ) ∈+′′+E } ∪ {ev | (ev , ve ) ∈ E }.

5. 2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case
For simplicity, we ﬁrst consider the case wherefe(ex) = f (ex) : Zn → Z is a one-dimensional ranking
function. Our aim is to ﬁnd a ranking function f (ex)
for E + , which satisﬁes ∀(ev , ve′ ) ∈ E + . f (ev ) > f (ev′ )and ∀(ev , ve′ ) ∈ E + . f (ev ) ≥ 0. If our ranking function
synthesizer ﬁnds such a ranking function f (ex), thena candidate well-founded relation Rf is constructed
as Rf (ex, xe′ ) := f (ex) ≥ 0 ∧ f (ex) > f (ex′ ).
Our synthesizer builds a decision tree D to ﬁnd aranking function fD (ex) for E + . The main question
in doing so is “when and how should we reﬁne partitions of decision trees?” To answer this question,
we consider the case where there is no ranking function fD (ex) for E + with a ﬁxed segmentation S, andclassify reasons for this into three cases as follows.
Case 1: explicit cycles in examples.
We deﬁne an explicit cycle in E + as a cycle in thegraph (Zn , E + ). An explicit cycle witnesses that
there is no ranking function for E + (see e.g., Example 4).
Case 2: non-crossing examples are unsatisﬁable.
The second case is when there is a leaf L ∈ S suchthat no aﬃne (not piecewise aﬃne) ranking func+of non-crossing examples extion for the set EL,L
ists. This prohibits the existence of piecewise aﬃnefunction fD (ex) for E + with segmentation S = S(D)because the restriction of fD (ex) to L ∈ S must be+.
an aﬃne ranking function for EL,L
Case 3: implicit cycles in the dependency
graph.
We deﬁne an implicit cycle by a cycle in the dependency graph G(S, E + ). Case 3 is the case wherean implicit cycle prohibits the existence of piecewiseaﬃne ranking functions for E + with the segmentation S (e.g., Example 5). If Case 1 and Case 2 do
not hold but no piecewise aﬃne ranking function
for E + with the segmentation S exists, then there
must be an implicit cycle by (the contraposition of)
the following proposition.
Proposition 16. Assume E + is a set of examples
that does not contain explicit cycles (i.e. Case 1
does not hold). Let S be a segmentation tree andassume that for each L ∈ S, there exists an aﬃne+ranking function fL (ex) for EL,L
(i.e. Case 2 does nothold). If the dependency graph G(S, E + ) is acyclic,
then there exists a decision tree D with the seg-mentation S(D) = S such that fD (ex) is a ranking
function for E + .
Proof. By induction on the height (i.e. the lengthof a longest path from a vertex) of vertices in
G(S, E + ). We construct a decision tree D as follows. If the height of L ∈ S is 0, then we assign fL′ (ex) := fL (ex) to the leaf L where fL (ex) is+a ranking function for EL,L
. If the height of L ∈ S
is n > 0, then we assign fL′ (ex) := fL (ex) + c to
the leaf L where c ∈ Z is a constant that satisﬁes+∀(ev , ve′ ) ∈ EL,Lv ) + c > fL′ ′ (ev ′ ) for each cell L′′ , fL (ewith the height less than n.
Note that the converse of Proposition 16 does nothold: the existence of implicit cycles in G(S, E + )does not necessarily imply that no piecewise aﬃneranking function exists with the segmentation S.
5. 3 Segmentation and (Explicit and Implicit) Cycles:
Multi-Dimensional
Lexicographic Case
We consider a more general case where fe(ex) =(fk (ex), . . . , f0 (ex)) is a multi-dimensional lexicographic ranking function and k is a ﬁxed nonnegative integer.
Given a function fe(ex), we consider the wellfounded relation Rfe(ex, xe′ ) deﬁned inductively as
follows. ′R() (ex, xe ) := ⊥R(fk ,...,f0 ) (ex, xe′ ) :=(10)fk (ex) ≥ 0 ∧ fk (ex) > fk (ex′ )∨ fk (ex) = fk (ex′ ) ∧ R(fk−1 ,...,f0 ) (e
x, x
e′ )
Our aim here is to ﬁnd a lexicographic ranking
function fe(ex) for E + , i.e. a function fe(ex) such thatRfe(ev , ve′ ) holds for each (ev , ve′ ) ∈ E + . Our synthesizer does so by building a decision tree. The same
argument as the one-dimensional case holds for lexicographic ranking functions.
Theorem 17 (cycle detection). Assume E + is aset of examples that does not contain explicit cycles. Let S be a segmentation tree and assume
that for each L ∈ S, there exists an aﬃne func+tion feL (ex) that satisﬁes ∀(ev , ve′ ) ∈ EL,L
, RfeL (ev , ve′ ).
+If the dependency graph G(S, E ) is acyclic, thenthere exists a decision tree D with the segmentation S(D) = S such that RfeD (ev , ve′ ) holds for each′+(ev , ve ) ∈ E .
Proof. The proof is almost the same as Proposi-Algorithm 1 Building decision trees.

Algorithm 2 Resolving Case 2.

Input: a set E of examples, an integer k ≥ 0
Output: a well-founded relation R such that∀(ex, xe′ ) ∈ E + , R(e
x, x
e′ )
1: if E has a cycle then2:
return unsatisﬁable
3: end if
4: D := ResolveCase2(E)5: while true do
6:
C := GetConstraints(D, E)
7:
O := SumAbsParams(D)8:ρ := Minimize(O, C)
9:
if ρ is deﬁned then10:fe(ex) := feρ(D) (ex)
11:
return Rfe
12:
else
13:
get an unsat core in C
14:
ﬁnd an implicit cycle (ev1 , ve1′ ), . . . , (evl , vel′ )in the unsat core15:
ﬁnd a cell C and two distinct pointsvei′ , vei+1 ∈ C in the implicit cycle
16:
add a halfspace to separate vei′ and vei+1
and update D
17:
end if
18: end while

1: function ResolveCase2(E ′+ )+tion 16. Here, note that if fe′ (ex) = fe(ex) + ec whereec is a tuple of nonnegative integer constants, thenx, xe′ ) subsumes Rfe(e
x, x
e′ ).
Rfe′ (e5. 4 Our Decision Tree Learning Algorithm
We design a concrete algorithm based on Theorem 17. It is shown in Algorithm 1 and consists ofthree phases. We shall describe the three phases
one by one.
Phase 1
Phase 1 (Line 1-3) detects explicit cycles in E +to exclude Case 1. Here, we use a cycle detection
algorithm for directed graphs.
Phase 2Phase 2 (Line 4) detects and resolves Case 2 byusing ResolveCase2 (Algorithm 2), which is afunction that grows a decision tree recursively. ResolveCase2 takes non-crossing examples in a leaf,

fe := MakeAffineTemplate(k)C := GetConstraints(fe, E ′+ )4:
ρ := GetModel(C)5:if ρ is undeﬁned then6:h := ChooseQualifier(E ′+ )7:D≥0 := ResolveCase2({(ev , ve′ ) ∈ E ′+ |′h(ev ) ≥ 0 ∧ h(ev ) ≥ 0})8:
D<0 := ResolveCase2({(ev , ve′ ) ∈ E ′+ |′h(ev ) < 0 ∧ h(ev ) < 0})9:
return (if h(ex) ≥ 0 then D≥0 else D<0 )
10:
else
11:
return fe
2:
3:

12:

end if

13: end function
14: function GetConstraints(D, E + )return {RfeD (ev , ve′ ) | (ev , ve′ ) ∈ E + } where
feD is the tuple of piecewise aﬃne functions corresponding to D
16: end function
15:

divides the leaf, and returns a template tree that isﬁne enough to avoid Case 2. Here, template trees
are decision trees whose leaves are labeled by aﬃnetemplates.
Algorithm 2 shows the detail of ResolveCase2.
ResolveCase2 builds a template tree recursively
starting from the trivial segmentation S = ⊥ andall given examples. In each polyhedron, ResolveCase2 checks whether the set C of constraints imposed by non-crossing examples can be satisﬁedby an aﬃne lexicographic ranking function on thepolyhedron (Line 2-3). If the set C of constraints
is not satisﬁable, then ResolveCase2 chooses ahalfspace h(ex) ≥ 0 (Line 6) and divides the current
polyhedron by the halfspace.
There is a certain amount of freedom in the
choice of halfspaces. To guarantee terminationof the whole algorithm, we require that the chosen halfspace h separates at least one point inE ′+ := {ev | (ev , ve′ ) ∈ E ′+ } ∪ {ev ′ | (ev , ve′ ) ∈ E ′+ }′+from the other points in E . That is:
Assumption 18. If halfspace h(ex) ≥ 0 is chosen
in Line 6 of Algorithm 2, then there exist ve, ue ∈ E ′+

Algorithm 3 A criterion for eager qualiﬁer selection.
1: function QualityMeasure(h, E ′+ )E++ := {(ev , ve′ ) ∈ E ′+ | h(ev ) ≥ 0∧h(ev ) ≥ 0}3:
E+− := {(ev , ve′ ) ∈ E ′+ | h(ev ) ≥ 0∧h(ev ) < 0}
′
′+
:=
4:
E−+
{(e
v , ve ) ∈ E | h(ev ) < 0∧h(ev ) ≥ 0}v , ve′ ) ∈ E ′+ | h(e5:E−− := {(ev ) < 0∧h(ev ) < 0}6:
fe := MakeAffineTemplate(k)7:
C+ := GetConstraints(fe, E++ )8:
C− := GetConstraints(fe, E−− )9:N+ := MaxSmt(C+ )10:
N− := MaxSmt(C− )11:return N+ + N− + (|E+− | + |E−+ |)(1 −entropy(|E+− |, |E−+ |))12: end function
2:such that h(ev ) ≥ 0 and h(eu) < 0.
We explain two strategies (eager and lazy) tochoose halfspaces that can be used to implement
ChooseQualifier. Both of them are guaranteed
to terminate, and moreover, intended to yield simple decision trees.
Eager strategy.
In the eager strategy, we eagerly generate a ﬁnite
set H of halfspaces from the set E + of all examples beforehand and choose the best one from H
with respect to a certain quality measure. To satisfy Assumption 18, H are generated so that any
two points ue, ve ∈ E + can be separated by some
halfspace (h(ex) ≥ 0) ∈ H.
For example, we can use intervals H = {±(xi −ai ) ≥ 0 | i = 1, . . . , n ∧ (a1 , . . . , an ) ∈ E + } andoctagons H = {±(xi − ai ) ± (xj − aj ) ≥ 0 | i ̸=j ∧ (a1 , . . . , an ) ∈ E + } where x
e = (x1 , . . . , xn ). For
any input E ′+ ⊆ E + of ResolveCase2, intervals
and octagons satisfy ∅ ̸= H ′ := {h(ex) ≥ 0 | ∃ev, ue∈E ′+ .h(ev ) ≥ 0 ∧ h(eu) < 0}, so Assumption 18 is satisﬁed by choosing the best halfspace with respect
to the quality measure from H ′ .
For each halfspace (h(ex) ≥ 0) ∈ H ′ , we calculate
QualityMeasure in Algorithm 3, and choose onethat maximizes QualityMeasure(h, E ′+ ). QualityMeasure(h, E ′+ ) calculates the sum of the
maximum number of satisﬁable constraints in eachleaf divided by h(ex) ≥ 0 plus an additionalterm (|E+− | + |E−+ |)(1 − entropy(|E+− |, |E−+ |))yxxwhere entropy(x, y) = − x+ylog2 x+y− x+yylog2 x+y . Therefore, the term (|E+− | + |E−+ |)(1 −entropy(|E+− |, |E−+ |)) is close to |E+− | + |E−+ | if
almost all examples in E+− ∪ E−+ cross h in thesame direction and close to 0 if |E+− | is almost
equal to |E−+ |.
Lazy strategy.
In the lazy strategy, we lazily generate halfspaces. We divide the current polyhedron so that
non-crossing examples in the cell point to almost
the same direction.
+
First, we label states that occur in EC,C
as follows. We ﬁnd a direction that most examples
in C point to by solving the MAX-SMT ⃗a :=+max⃗a {(ev , ve′ ) ∈ EC,C
| ⃗a · (ev − ve′ ) > 0} . For each+′(ev , ve ) ∈ EC,C , we label two points ve, ve′ with +1 if⃗a · (ev − ve′ ) > 0 and with −1 otherwise.
Then we apply weighted C-SVM to generate a
hyperplane that separates most of the positive andnegative points. To guarantee termination of Algorithm 1, we avoid “useless” hyperplanes that classify all the points by the same label. If we obtainsuch a useless hyperplane, then we undersample amajority class and apply C-SVM again. By undersampling suitably, we eventually get linearly separable data with at least one positive point and one
negative point.
Note that since coeﬃcients of hyperplanes extracted from C-SVM are ﬂoating point numbers,
we have to approximate them by hyperplanes withrational coeﬃcients. This is done by truncating
continued fraction expansions of coeﬃcients by asuitable length.
Phase 3
In Line 5-18 of Algorithm 1, we further reﬁne thesegmentation S(D) to resolve Case 3. Once Case 2
is resolved by ResolveCase2, Case 2 never holds
even after reﬁning S(D) further. This enables toseparate Phases 2 and 3.
Given a template tree D, we consider the set C ofconstraints on parameters in D that claims feD (ex)
is a ranking function for E + (Line 6).
If C is satisﬁable, we use an SMT solver to obtaina solution of C (i.e. an assignment ρ of integers toparameters) while minimizing the sum of absolutevalues of unknown parameters in D at the sametime (Line 8). This minimization is intended togive a simple candidate ranking function. The so-lution ρ is used to instantiate the template tree D(Line 11).
If C cannot be satisﬁed, there must be an implicit cycle in the dependency graph G(S(D), E + )by Theorem 17. The implicit cycle can be found in
an unsatisﬁable core of C. We reﬁne the segmentation of D to cut the implicit cycle in Line 16. To
guarantee termination, we choose a halfspace satisfying the following assumption, which is similar toAssumption 18.
Assumption 19. If halfspace h(ex) ≥ 0 is chosen inLine 16 of Algorithm 1, then there exist ve, ue ∈ E+
such that h(ev ) ≥ 0 and h(eu) < 0.
We have two strategy (eager and lazy) to reﬁnethe segmentation of D.
In eager strategy, we choose a halfspace (h(ex) ≥0) ∈ H that separates two distinct points vei′
and vei+1 in the implicit cycle. In doing so, wewant to reduce the number of implicit cycles in
G(S(D), E + ), but adding a new halfspace may introduce new implicit cycles if there exists (ev , ve′ ) ∈+EC,C that crosses the new border from the side of vei′
to the side of vei+1 . Therefore, we choose a hyperplane that minimizes the number of new crossing
examples.
In lazy strategy, we use an SMT solver to ﬁnda hyperplane h(ex) ∈ H that separates vei′ and vei+1
and minimizes the number of new crossing examples.
Termination
Assumption 18 and Assumption 19 guarantees
that every leaf in S(D) contains at least one pointin the ﬁnite set E + . Because the number of leavesin S(D) strictly increases after each iteration of
Phase 2 and Phase 3, we eventually get a segmentation S(D) where each L ∈ S(D) contains only one
point in E + in the worst case. Since we have excluded Case 1 at the beginning, Theorem 17 guarantees the existence of ranking function with thesegmentation S(D). Therefore, the algorithm terminates within |E + | times of reﬁnement.
Theorem 20. If Assumption 18 and Assumption 19 hold, then Algorithm 1 terminates. If Algorithm 1 returns a piecewise aﬃne lexicographic
function fe(ex), then the function satisﬁes Rfe(e
x, x
e′ )
′
+
+
for each (ex, xe ) ∈ E where E is the input of thealgorithm.
5. 5 Improvement by Degenerating Nega-tive Values
There is another way to deﬁne well-founded relation from the tuple fe(ex) = (fk (ex), . . . , f0 (ex))
of functions, that is, the well-founded relation′
Rf′e(ex, xe′ ) deﬁned inductively by R()(ex, xe′ ) := ⊥ and′′R(fk ,...,f0 ) (ex, xe ) := fk (ex) ≥ 0 ∧ fk (ex) > fk (ex′ ) ∨

′
′
′
fk (e
x ) < 0 ∨ fk (ex) = fk (ex ) ∧ R(fk−1 ,...,f0 ) (e
x, x
e′ ).
In this deﬁnition, we loosen the equality fi (e
x) =
′
fi (e
x ) (where i = 1, . . . , k) of the usual lexicographic ordering (10) to fi (ex′ ) < 0 ∨ fi (ex) = fi (ex′ ).
This means that once fi (ex) becomes negative, fi (ex)
must stay negative but the value do not have tobe the same, which is useful for the synthesizer
to avoid complex candidate lexicographic ranking
functions and thus improves the performance.
However, if we use this well-founded relationx, xe′ ) instead of Rfe(ex, xe′ ) in (10), then TheRf′e(e′x, xe′ ) is not necessarily
orem 17 fails because Rfe(ec = (ck , . . . , c0 ) is a nonsubsumed by Rf′e+ec where enegative constant (see the proof of Proposition 16
and Theorem 17). As a result, there is a chancethat no implicit cycle can be found in line 14 ofx, xe′ ), weAlgorithm 1. Therefore, when we use Rf′e(emodify Algorithm 1 so that if no implicit cycle canbe found in line 14, then we fall back on the former
deﬁnition of Rfe(ex, xe′ ) and restart Algorithm 1.

6 Implementation and Evaluation
Implementation.
We implemented a constraint solver MuVal that
supports invariant synthesis and ranking function
synthesis. For invariant synthesis, we apply an ordinary decision tree learning (see [12, 14, 18, 22, 35]
for existing techniques). For ranking function synthesis, we implemented the algorithm in Sect. 5with both eager and lazy strategies for halfspace
selection. Our synthesizer uses well-founded relation explained in Sect. 5. 5. Given a benchmark,we run our solver for both termination and nontermination veriﬁcation in parallel, and when oneof the two returns an answer, we stop the otherand use the answer. MuVal is written in OCaml
and uses Z3 as an SMT solver backend. We usedclang and llvm2kittel [1] to convert C benchmarks
to T2 [3] format ﬁles, which are then translated to
pwCSP by MuVal.

100

MuVal

Table 2: Numbers of solved benchmarks
Yes No TO U
MuVal (eager)
204 89 42 0
MuVal (lazy)200 84 51 0
AProVE
216 100 16 3
iRankFinder
208 92†1 0 34
Ultimate Automizer 180 83 2 70

10

1

1

10

100

AProve†1 We removed one benchmarks from the result ofiRankFinder because the answer was wrong.

MuVal

100

10

1

1

10

100

irankfinder v1.3.2

100

MuVal

Experiments.
We evaluated our implementation MuVal on C
benchmarks from Termination Competition 2020
(C Integer) [4].
We compared our tool with
AProVE [10, 13], iRankFinder [7], and Ultimate Automizer [21]. Experiments are conducted
on StarExec [2] (CentOS 7.7 (1908) on Intel(R)Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ)
with 263932744 kB main memory). The time limit
was 300 seconds.
Results.
Results are shown in Table 2. Yes/No/TO/U
means the number of benchmarks that thesetools could verify termination/could verify nontermination/could not answer within 300 seconds
and timed out (TimeOut)/gave up before 300 seconds (Unknown), respectively. We also show scatter plots of runtime in Fig. 7.
MuVal was able to solve more benchmarks thanUltimate Automizer.
Compared to iRankFinder, MuVal solved slightly fewer benchmarks,
but was faster in a large number of benchmarks:
265 benchmarks were solved faster by MuVal, 68
by iRankFinder, and 2 were not solved by bothtools within 300 seconds (here, we regard U (unknown) as 300 seconds). Compared to AProVE,
MuVal solved fewer benchmarks. However, there
are several benchmarks that MuVal could solve
but AProVE could not. Among them is “TelAvivAmir-Minimum true-termination.c”, which does
require piecewise aﬃne ranking functions. MuVal found a ranking function f (x, y) = if x − y ≥0 then y else x, while AProVE timed out.
We also observed that using CEGIS with transition examples itself showed its strengths even forbenchmarks that do not require piecewise aﬃneranking functions. Notably, there are three bench-

10

1

1

10

100

Ultimate Automizer

Fig. 7: Scatter plots of runtime. Ultimate Automizer and AProVE sometimes gave up before
the time limit, and such cases are regarded as 300s.
marks that MuVal could solve but the other tools
could not; they are examples that do not require segmentations. Further analysis of thesebenchmarks indicates the following strengths of ourframework: (1) the ability to handle nonlinear constraints (to some extent) thanks to the examplebased synthesis and the recent development of SMT
solvers; and (2) the ability to ﬁnd a long lassoshaped non-terminating trace assembled from multiple transition examples. See Appendix A for details.

7 Related Work
There are a bunch of works that synthesize ranking functions via constraint solving. Among them isa counterexample-guided method like CEGIS [28].
CEGIS is sound but not guaranteed to be complete in general: even if a given constraint has asolution, CEGIS may fail to ﬁnd the solution. A
complete method for ranking function synthesis is
proposed in [19]. They collect only extremal counterexamples instead of arbitrary transition examples to avoid inﬁnitely many examples. A limitation of their method is that the search space is limited to (lexicographic) aﬃne ranking functions.
Another counterexample-guided method is proposed in [32] and implemented in SeaHorn. Thismethod can synthesize piecewise aﬃne functions,but their approach is quite diﬀerent from ours.
Given a program, they construct a safety property
that the number of loop iterations does not exceed
the value of a candidate ranking function. The
safety property is checked by a veriﬁer. If it is violated, then a trace is obtained as a counterexample
and the candidate ranking function is updated by
the counterexample. The main diﬀerence from our
method is that their method uses trace examples
while our method uses transition examples (whichis less expensive to handle). FreqTerm [15] alsouses the connection to safety property, but they exploit syntax-guided synthesis for synthesizing ranking functions.
Aside from counterexample-guided methods,
constraint solving is widely studied for aﬃne ranking functions [26], lexicographic aﬃne ranking functions [5, 7, 23], and multiphase aﬃne ranking functions [6, 8]. Their implementation includes RankFinder and iRankFinder. Farkas’ lemma or
Motzkin’s transposition theorem are often used asa tool to transform ∃∀-constraints to ∃-constraints.
However, when we apply this technique to piecewise aﬃne ranking functions, we get nonlinear constraints [23].
Abstract interpretation is also applied to segmented synthesis of ranking functions and implemented in FuncTion [31, 33, 34]. In this series ofwork, decision tree representation of ranking functions is used in [34] for better handling of disjunctions. Compared to their work, we believe that our
method is more easily extensible to other theories
than linear integer arithmetic as long as the theories are supported by SMT solvers (although suchextensions are out of the scope of this paper).
Other state-of-the-art termination veriﬁers include the following. Ultimate Automizer [21] is
an automata-based method. It repeatedly ﬁnds a
trace and computes a termination argument that

contains the trace until termination arguments
cover the set of all traces. Büchi automata are used
to handle such traces. AProVE [10,13] is based onterm rewriting systems.

8 Conclusions and Future WorkIn this paper, we proposed a novel decision treebased synthesizer for ranking functions, which is
integrated into the CEGIS architecture. The key
observation here was that we need to cope with
explicit and implicit cycles contained in given examples. We designed a decision tree learning algorithm using the theoretical observation of the cycle
detection theorem. We implemented the frameworkand observed that its performance is comparable tostate-of-the-art termination analyzers. In particular, it solved three benchmarks that no other tool
solved, a result that demonstrates the potential of
the current combination of CEGIS, segmented synthesis, and transition examples.
We plan to extend our ranking function synthesizer to a synthesizer of piecewise aﬃne ranking supermartingales. Ranking supermartingales [11] areprobabilistic version of ranking functions and usedfor veriﬁcation of almost-sure termination of probabilistic programs.
We also plan to implement a mechanism toautomatically select a suitable set of halfspaces
with which decision trees are built. In our ranking function synthesizer, intervals/octagons/octahedron/polyhedra can be used as the set of halfspaces. However, selecting an overly expressive
set of halfspaces may cause the problem of overﬁtting [24] and result in poor performance. Therefore,
applying heuristics that adjusts the expressivenessof halfspaces based on the current examples may
improve the performance of our tool.
Acknowledgement.
We thank Andrea Peruﬀo and the anonymousreferees for many suggestions. This work was supported by JST ERATO HASUO Metamathematics
for Systems Design Project (No. JPMJER1603)
and JSPS KAKENHI Grant Numbers 20H04162,
20H05703, 19H04084, and 17H01720.
References[ 1 ] : llvm2KITTeL, https://github.com/hkhlaaf/
llvm2kittel.

[ 2 ] : StarExec, https://www.starexec.org.
[ 3 ] : T2 TEMPORAL LOGIC PROVER, https://github.com/mmjb/T2.
[ 4 ] : Termination Competition 2020: C Integer, https://termcomp.github.io/Y2020/job 41519.
html.
[ 5 ] Alias, C., Darte, A., Feautrier, P., and Gonnord,
L.: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, SAS ’10, Springer, 2010, pp. 117–133.
[ 6 ] Ben-Amram, A. M., Doménech, J. J., andGenaim, S.: Multiphase-Linear Ranking Functions
and Their Relation to Recurrent Sets, SAS ’19,
Springer, 2019, pp. 459–480.
[ 7 ] Ben-Amram, A. M. and Genaim, S.: Ranking
Functions for Linear-Constraint Loops, Journal of
the ACM, Vol. 61, No. 4(2014).
[ 8 ] Ben-Amram, A. M. and Genaim, S.: On
Multiphase-Linear Ranking Functions, CAV ’17,
Springer, 2017, pp. 601–620.
[ 9 ] Bjørner, N., Gurﬁnkel, A., McMillan, K. L., andRybalchenko, A.: Horn Clause Solvers for Program
Veriﬁcation, Fields of Logic and Computation II:
Essays Dedicated to Yuri Gurevich on the Occasionof His 75th Birthday, LNCS, Vol. 9300, Springer,
2015, pp. 24–51.
[10] Brockschmidt, M., Ströder, T., Otto, C., andGiesl, J.: Automated Detection of Non-termination
and NullPointerExceptions for Java Bytecode,
FoVeOOS ’11, LNCS, Vol. 7421, Springer, 2012,
pp. 123–141.
[11] Chakarov, A. and Sankaranarayanan, S.: Probabilistic Program Analysis with Martingales, Computer Aided Veriﬁcation, Hutchison, D., Kanade,T., Kittler, J., Kleinberg, J. M., Mattern,F., Mitchell, J. C., Naor, M., Nierstrasz, O.,
Pandu Rangan, C., Steﬀen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M. Y., Weikum,
G., Sharygina, N., and Veith, H.(eds.), Vol. 8044,
Springer Berlin Heidelberg, Berlin, Heidelberg,
2013, pp. 511–526.
[12] Champion, A., Chiba, T., Kobayashi, N., andSato, R.: ICE-Based Reﬁnement Type Discovery
for Higher-Order Functional Programs, TACAS ’18,
LNCS, Vol. 10805, Springer, 2018, pp. 365–384.
[13] Emmes, F., Enger, T., and Giesl, J.: Proving Non-looping Non-termination Automatically,
IJCAR ’12, LNCS, Vol. 7364, Springer, 2012,
pp. 225–240.
[14] Ezudheen, P., Neider, D., D’Souza, D., Garg,
P., and Madhusudan, P.: Horn-ICE Learning for
Synthesizing Invariants and Contracts, Proceedingsof the ACM on Programming Languages, Vol. 2,
No. OOPSLA(2018), pp. 131:1–131:25.
[15] Fedyukovich, G., Zhang, Y., and Gupta, A.:
Syntax-Guided Termination Analysis, CAV ’18,
LNCS, Vol. 10981, Springer, 2018, pp. 124–143.
[16] Floyd, R. W.: Assigning Meanings to Programs,

Proceedings of Symposium on Applied Mathematics,
Vol. 19(1967), pp. 19–32.
[17] Garg, P., Löding, C., Madhusudan, P., and Neider, D.: ICE: A Robust Framework for Learning
Invariants, CAV ’14, Springer, 2014, pp. 69–87.
[18] Garg, P., Neider, D., Madhusudan, P., and Roth,D.: Learning Invariants Using Decision Trees and
Implication Counterexamples, POPL ’16, ACM,
2016, pp. 499–512.
[19] Gonnord, L., Monniaux, D., and Radanne, G.:
Synthesis of Ranking Functions Using Extremal
Counterexamples, PLDI ’15, ACM, 2015, pp. 608–
618.
[20] Gupta, A., Henzinger, T. A., Majumdar, R.,
Rybalchenko, A., and Xu, R.-G.: Proving nontermination, POPL ’08, ACM, 2008, pp. 147–158.
[21] Heizmann, M., Hoenicke, J., and Podelski, A.:
Termination Analysis by Learning Terminating Programs, CAV ’14, Springer, 2014, pp. 797–813.
[22] Krishna, S., Puhrsch, C., and Wies, T.:
Learning Invariants using Decision Trees, CoRR,
Vol. abs/1501.04725(2015).
[23] Leike, J. and Heizmann, M.: Ranking Templatesfor Linear Loops, TACAS ’14, LNCS, Vol. 8413,
Springer, 2014, pp. 172–186.
[24] Padhi, S., Millstein, T. D., Nori, A. V., andSharma, R.: Overﬁtting in Synthesis: Theory andPractice, CAV ’19, LNCS, Vol. 11561, Springer,
2019, pp. 315–334.
[25] Padhi, S., Sharma, R., and Millstein, T. D.:
Data-Driven Precondition Inference with Learned
Features, PLDI ’16, 2016, pp. 42–56.
[26] Podelski, A. and Rybalchenko, A.: A Complete
Method for the Synthesis of Linear Ranking Functions, VMCAI ’04, LNCS, Vol. 2937, Springer, 2004,
pp. 239–251.
[27] Satake, Y., Unno, H., and Yanagi, H.: Probabilistic Inference for Predicate Constraint Satisfaction, Proceedings of AAAI 2020, 2020.
[28] Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., and Saraswat, V.: Combinatorial Sketching for Finite Programs, ASPLOS XII, ACM, 2006,
pp. 404–415.
[29] Unno, H., Satake, Y., Terauchi, T., andKoskinen, E.: Program Veriﬁcation via Predicate
Constraint Satisﬁability Modulo Theories, CoRR,
Vol. abs/2007.03656(2020).
[30] Unno, H., Terauchi, T., and Koskinen, E.:
Constraint-based Relational Veriﬁcation, CAV ’21,
Springer, 2021.
[31] Urban, C.: The Abstract Domain of Segmented
Ranking Functions, SAS ’13, LNCS, Vol. 7935,
Springer, 2013, pp. 43–62.
[32] Urban, C., Gurﬁnkel, A., and Kahsai, T.: Synthesizing Ranking Functions from Bits and Pieces,
TACAS ’16, Springer, 2016, pp. 54–70.
[33] Urban, C. and Miné, A.: An Abstract Domain
to Infer Ordinal-Valued Ranking Functions, ESOP

’14, Springer, 2014, pp. 412–431.
[34] Urban, C. and Miné, A.: A Decision Tree Abstract Domain for Proving Conditional Termination, SAS ’14, Springer, 2014, pp. 302–318.
[35] Zhu, H., Magill, S., and Jagannathan, S.: A
Data-driven CHC Solver, PLDI ’18, ACM, 2018,
pp. 707–721.

A Detailed Discussion of The Experiment
We show some of the benchmarks from Termination Competition 2020 that are solved by MuVal
but not by AProVE, Ultimate Automizer, andiRankFinder. We also discuss the strength of our
method.
A benchmark containing a nonlinear operation.
Fig. 8a shows one of the benchmarks that contains a nonlinear operation y = y * y but admits
a linear ranking function. Although handling nonlinear operation is diﬃcult in general, MuVal wasable to verify termination. The reason can be understood as follows. (1) Our validator can ﬁnd transition examples for this benchmark thanks to therecent development of SMT solvers. (2) Our syn-thesizer can work as usual because it is examplebased.
A benchmark that requires a long lassoshaped non-terminating trace to prove
non-termination.
Fig. 8b is a benchmark that is non-terminating.
To prove non-termination of this benchmark, weneed to ﬁnd a long lasso-shaped trace that ends inthe self loop when i = range = 0. Finding sucha long lasso is diﬃcult in general, but MuVal wasable to ﬁnd one in this benchmark: during CEGIS
iterations, MuVal found the self loop (i.e. explicit
cycle) and then collected transition examples thatwere needed to prove reachability of cycles.
Our method can naturally collect transition examples “backward” from the self loop (an explicit
cycle). At the same time, our method collects transition examples “forward” from an initial state (inthe benchmark of Fig. 8b, the pair of i = 10 andrange = 20 is an initial state of the while loop).
When transition examples that are collected backward and forward form a trace to the self loop,
our method notice that the benchmark is nonterminating.

int main () {int x = ?;int y = 2;
int res = 1;
if ( x < 0 || y < 1) { }else {
while ( x > y ) {y = y*y;res = 2* res ;}}}(a) A benchmark containing a nonlinear operation.
int main () {int i = ?;int range = 20;
while (0 <= i && i <= range ) {if (!(0 == i && i == range )) {if ( i == range ) {i = 0;
range = range -1;} else {i = i +1;}}}}(b) A benchmark that requires a long lasso to prove
non-termination

Fig. 8: Some of the benchmarks