Decision Tree Learning in
CEGIS-Based Termination Analysis

Satoshi Kura1,2

Hiroshi Unno3,4

Ichiro Hasuo1,2

1 National Institute of Informatics, Tokyo, Japan
2 The Graduate University for Advanced Studies (SOKENDAI), Kanagawa, Japan
3 University of Tsukuba, Ibaraki, Japan
4 RIKEN AIP, Tokyo, Japan

Termination Analysis“Does this program terminate (or not)?”
Many methods based on ranking function synthesis• Example-based[Urban et al., TACAS’16], [Fedyukovich et al., CAV’18], [Gonnord et al., PLDI’15]• ω-automata-based [Heizmann et al., CAV’14]• Abstract interpretation [Urban, SAS’13]

Satoshi Kura (NII, Tokyo)

1

Our Contribution
We propose an example-based termination analyzer.
Specifically, we use ...
• CEGIS architecture [Solar-Lezama et al., ASPLOS’06]• transition examples collected by SMT solvers• decision tree learning to obtain piecewise affine
ranking functions.
We obtained promising experimental results.

Satoshi Kura (NII, Tokyo)

2Comparison with Other Example-Based Methods• trace examples (collected by safety verifiers)[Urban et al., TACAS’16], [Fedyukovich et al., CAV’18]• transition examples (collected by SMT solvers)• affine ranking function[Gonnord et al., PLDI’15]• piecewise affine ranking function
our work

Satoshi Kura (NII, Tokyo)

3

Decision Tree Learning in CEGIS• for invariant synthesis (state examples)[Champion et al., TACAS’18], [Ezudheen et al., OOPSLA’18], ..

• for ranking function synthesis (transition examples)
our work

Satoshi Kura (NII, Tokyo)

4Outline

Termination Problem and CEGISOur Synthesizer

Experimental Results

Satoshi Kura (NII, Tokyo)

5

Ranking Function [Floyd, ’67]
Let S be a state space.
Let τ ⊆ S × S be a transition relation.
f : S → Z is a ranking function if for each (x, x0 ) ∈ τ• f (x) ≥ 0• f (x) > f (x0 )If such a ranking function exists, then τ terminates.

Satoshi Kura (NII, Tokyo)

6Termination Problem to Constraint Solving
Given a program, consider the following problems.
Find a (ranking) function f (x) s.t.
(x, x0 ) ∈ τ=⇒

R(x, x0 )where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

while (x != 0) {if (x > 0) x--;else x++; }Satoshi Kura (NII, Tokyo)

x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)

7

CounterExample Guided Inductive Synthesis
CEGIS [Solar-Lezama et al., ASPLOS’06]
candidate solution
Synthesizer
No solution

constraints
Validator

set of examples

solution

CEGIS solves constraints via interaction between thesynthesizer and the validator.

Satoshi Kura (NII, Tokyo)

8

Synthesizer

candidate solution

Validator

Synthesizer
No solution

constraints

set of examples

solution

Given a set of (transition) examples,• return a candidate solution if exists• candidate solution = ranking function for examples• answer “no solution” otherwise
Satoshi Kura (NII, Tokyo)

9

Validator
constraints

candidate solution
Synthesizer
No solutionValidator
set of examples

solution

Given a candidate solution for the examples,• if the candidate solution is a genuine solution, returnthe solution• otherwise, add counterexamples to the set ofexamples using SMT solvers.
Satoshi Kura (NII, Tokyo)

10

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}
solution
f (x)
= |x|

A constraint satisfaction problem is given. The set ofexamples is ∅.
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)(x)==|x|x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}
solution
f (x)
= |x|

The synthesizer returns a candidate solution for ∅.
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)(x)==|x|x0Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}solutionf (x)= |x|

The validator finds a new counterexample R(1, 0).
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}
solution
f (x)
= |x|

The validator finds a new counterexample R(1, 0).
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}
solution
f (x)
= |x|

The synthesizer returns a candidate solution for{R(1, 0)}.
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}
solutionf (x)= |x|

The validator finds a new counterexample R(−2, −1).
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}solution
f (x)
= |x|

The validator finds a new counterexample R(−2, −1).
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}solution
f (x)
= |x|

The synthesizer returns a candidate solution for{R(1, 0), R(−2, −1)}.
Satoshi Kura (NII, Tokyo)

11

CEGIS Example
Constraints:
x 6= 0 ∧ x > 0 =⇒ R(x, x − 1)
x 6= 0 ∧ x ≤ 0 =⇒ R(x, x + 1)
where R(x, x0 ) := f (x) ≥ 0 ∧ f (x) > f (x0 ).

constraints

candidate:candidate: ff(x)
(x)=
=|x|
x0
Synthesizer

Validator

example:example:{R(1,example:{R(1,0), R(−2,∅ is0)}−1)}solution
f (x)
= |x|

The validator confirms that f (x) = |x| is a genuine
solution.
Satoshi Kura (NII, Tokyo)

11Outline

Termination Problem and CEGISOur Synthesizer

Experimental Results

Satoshi Kura (NII, Tokyo)

12

Overview of Our Synthesizer
constraintscandidate solution

Validator

Synthesizer
No solution

set of examples

solution• Input: a set of transition examples• Output: a candidate solution for the input• Search space: piecewise affine functions
xx≥07→f (x) =x−x x < 00
Satoshi Kura (NII, Tokyo)

13

Decision Tree Representation
To represent piecewise affine ranking functions,
our synthesizer uses decision trees.
• Node = halfspace (affine inequality)• Leaf = affine functiony≥0≥<x−1≥0−y≥<x−11−x

Satoshi Kura (NII, Tokyo)

f (x, y) =
x−1 y ≥0 ∧ x−1≥0
1−x y ≥0 ∧ x−1<0−yy<014

Outline of Our Algorithm
Key idea: handling cycles in transition examples
1. Detect explicit cycles• Proceed if no explicit cycle exists

2. Refine the current segmentation• We get a decision tree that ranks “non-crossingexamples”.

3. Cut implicit cycles• Eventually, there is no implicit cycle.
• We get a decision tree that ranks all examples.
Satoshi Kura (NII, Tokyo)

15

Phase 1: Detect Explicit Cycles
If{R(a1 , a2 ), R(a2 , a3 ), . . . , R(an , a1 ), . . . }isgiven as examples,a3a1a2

this witnesses non-termination.
We call this an explicit cycle.

Satoshi Kura (NII, Tokyo)

16

Outline of Our Algorithm
1. Detect explicit cycles• Proceed if no explicit cycle exists

2. Refine the current segmentation• We get a decision tree that ranks “non-crossingexamples”.

3. Cut implicit cycles• Eventually, there is no implicit cycle.
• We get a decision tree that ranks all examples.

Satoshi Kura (NII, Tokyo)

17

Phase 2: Refine the Current Segmentation
examplesdecision tree
No affineranking function?

x

Divide state spacex≥0x

Satoshi Kura (NII, Tokyo)?

by good halfspace?

18

Phase 2: Refine the Current Segmentation
examplesdecision tree
No affineranking function?

x

Divide state space

x≥0x

?

by good halfspace?

... until each leaf has an affine ranking function.
Satoshi Kura (NII, Tokyo)

18

Phase 2: Refine the Current Segmentation
examplesdecision tree
No affineranking function?

x

Divide state spacex≥0xx

by good halfspace−x... until each leaf has an affine ranking function.
Satoshi Kura (NII, Tokyo)

18

Outline of Our Algorithm
1. Detect explicit cycles• Proceed if no explicit cycle exists

2. Refine the current segmentation• We get a decision tree that ranks “non-crossingexamples”.

3. Cut implicit cycles• Eventually, there is no implicit cycle.
• We get a decision tree that ranks all examples.

Satoshi Kura (NII, Tokyo)

19

Crossing Examples
If a “crossing example” exists after Phase 2,functions at each leaf cannot be determined
independently.

x≥0−1

Satoshi Kura (NII, Tokyo)

1xx−x

20

Crossing Examples
If a “crossing example” exists after Phase 2,
functions at each leaf cannot be determinedindependently.

x≥0−1

1xx−xx ranks all transition examples in x ≥ 0.

Satoshi Kura (NII, Tokyo)

20

Crossing Examples
If a “crossing example” exists after Phase 2,
functions at each leaf cannot be determined
independently.

x≥0−1

1xx−x

−x ranks all transition examples in x < 0.

Satoshi Kura (NII, Tokyo)

20

Crossing Examples
If a “crossing example” exists after Phase 2,
functions at each leaf cannot be determined
independently.

x≥0−1

1xx−x

f (x) = if x ≥ 0 then x else − xdoes NOT rank the crossing example.
Satoshi Kura (NII, Tokyo)

f (−1) ≯ f (1)20

Crossing Examples
If a “crossing example” exists after Phase 2,
functions at each leaf cannot be determined
independently.

x≥0−1

1xx−x + 1

We need to add some constant.
f (x) = if x ≥ 0 then x else − x + 1
Satoshi Kura (NII, Tokyo)

20

Cycle Detection Theorem
Given a decision tree that ranks non-crossing examples,x≥0x<0x≥0x−x
let G be the graph induced by crossing examples.
x<0x≥0Theorem.
If G is acyclic, then there is a decision tree for all transition examples without changing the segmentation.
Satoshi Kura (NII, Tokyo)

21

Phase 3: Cut Implicit Cycles
By the cycle detection theorem,
it suffices to handle the following case.

If there is such an “implicit cycle”, then cut the cycle.

Satoshi Kura (NII, Tokyo)

22

Phase 3: Cut Implicit Cycles
By the cycle detection theorem,
it suffices to handle the following case.

If there is such an “implicit cycle”, then cut the cycle.

Repeat this until no implicit cycle.
Satoshi Kura (NII, Tokyo)

22

Outline of Our Algorithm
1. Detect explicit cycles• Proceed if no explicit cycle exists

2. Refine the current segmentation• We get a decision tree that ranks “non-crossingexamples”.

3. Cut implicit cycles• Eventually, there is no implicit cycle.
• We get a decision tree that ranks all examples.

Satoshi Kura (NII, Tokyo)

23

Outline

Termination Problem and CEGISOur Synthesizer

Experimental Results

Satoshi Kura (NII, Tokyo)

24

Setting• Our tool (MuVal)• Synthesizer: Phase 1-3 + two heuristics (eager/lazy)
to obtain simple candidates• Benchmarks: Termination Competition 2020 (CInteger)• Compared with AProVE, iRankFinder, and UltimateAutomizer• Environment: StarExec (https://www.starexec.org/)

Satoshi Kura (NII, Tokyo)

25

Number of Solved Benchmarks
Yes NoTimeout

Unknown(300 s)(give up)

MuVal (eager)

204 89420

MuVal (lazy)200 84510AProVE

216 100

163iRankFinder

208 92034

Ultimate Automizer

180 83270• Ultimate Automizer < MuVal < iRankFinder < AProVE

Satoshi Kura (NII, Tokyo)

26

Runtime
100

10100

MuVal

MuVal

MuVal

100

1011110100

1110irankfinder v1.3.2

AProve10100

110100Ultimate Automizer

Lower triangle = MuVal is faster• MuVal solved faster than iRankFinder in 265 / 335
benchmarks.

Satoshi Kura (NII, Tokyo)

27

Selected Benchmarks
Some of the benchmarks are solved by MuVal but not by
AProVE.
• TelAviv-Amir-Minimum_true-termination.c• Requires piecewise affine ranking functionsf (x, y) = min{x, y}• Solved by MuVal but not by AProVE.

• LogMult.c• Contains nonlinear transition (y = y * y;)• Has affine ranking function• Solved only by MuVal
Satoshi Kura (NII, Tokyo)

28

Conclusions and Future WorkConclusions• Decision tree learning for ranking function synthesis• Promising experimental results• MuVal solved more than Ultimate Automizer.
• MuVal solved faster than iRankFinder.
• Some benchmarks were solved only by MuVal.

Future work
• Improving performance by combining ML• Extension to ranking supermartingale synthesis
Satoshi Kura (NII, Tokyo)

29