### tptx - Stanford University

```Aditya Nori
Rahul Sharma
MSR India
Stanford University

Prove termination of a program

Program terminates if all loops terminate

Hard problem, undecidable in general

Need to exploit all available information

Previous techniques are static
 Tests are a neglected source of information

Tests have previously been used
 Safety properties, empirical complexity, …

This work, use tests for termination proofs
gcd(int x,int y)
assume(x>0 && y>0);
while( x!=y ) do
if( y > x )
y = y–x;
if( x > y)
x = x-y;
od
return x;
x=1, y=1
x=2, y=1
⋮
…
while …
…
…
while …
print x
print y
(1,1)
(2,1)
⋮
Data
ML
…
while …
…
assert …
x=1, y=3
…
while …
…
…
while …
print x
print y
(1,1)
(2,1)
⋮
Data
ML
…
while …
…
assert …
x=1, y=3
gcd(int x, int y)
assume(x>0 && y>0);
a := x; b := y;
c := 0;
while( x!=y ) do
c := c + 1;
if( y > x )
y := y–x;
if( x > y)
x := x-y;
od
print ( a, b, c );

New variables to
capture initial values

Introduce a loop counter

Print values of input
variables and counter
…
while …
…
…
while …
print x
print y
(1,1)
(2,1)
⋮
Data
ML
…
while …
…
assert …
x=1, y=3
gcd(int x, int y)
assume(x>0 && y>0);
a := x; b := y;
c := 0;
while( x!=y ) do
c := c + 1;
if( y > x )
y := y–x;
if( x > y)
x := x-y;
od
print( a, b, c)
≡
1
1 1
1 2
1 1

1
1
3

0
≡
1
2
For  ∈ ℕ, on inputs  ,
the loop iterates  times
Infer a bound using  and
…
while …
…
…
while …
print x
print y
(1,1)
(2,1)
⋮
Data
ML
…
while …
…
assert …
x=1, y=3

Predict number of iterations (final value of c)
 As a linear expression in a and b
 Find w1 , w2 , w3 : 1 + 2  + 3  ≈
 Find w1 , w2 , w3 : min

=1
1 + 2  + 3  −
 But we want 1 + 2  + 3  ≥
▪ Add 1 + 2  + 3  ≥  as a constraint
2

1
min    −
2
. .  ≥

Solved in MATLAB

For gcd example,  = [−2,1,1]
 Bound  ≤  +  − 2
…
while …
…
…
while …
print x
print y
(1,1)
(2,1)
⋮
Data
ML
…
while …
…
assert …
x=1, y=3
assume(x>0 && y>0);
 Bound:  ≤  +  − 2
a := x; b := y;
c := 0;
 Difficult to validate
while( x!=y ) do
c := c + 1;
 Infer invariants from tests
if( y > x )
y := y–x;
if( x > y)
x := x-y;
assert(c <= a+b-2);
od
assume(x>0 && y>0);
a := x; b := y; c := 0;
while( x!=y ) do
print(c, a, b, x, y);
c := c + 1;
if( y > x )
y := y–x;
if( x > y)
x := x-y;
assert(c <= a+b-2);
od

Predict a bound on c

Same tests, more data

Solve same QP

has five columns
 [1,a,b,x,y]

has c at every iteration
assume(x>0 && y>0);

a:=x; b:=y; c := 0;
free_inv(c<=a+b-x-y); 
while( x!=y ) do
c := c + 1;

if( y > x )

y := y – x;
if( x > y)
x := x-y;
assert(c <= a+b-2 );
od
Obtain  ≤  +  −  −
Use if checker can prove

Give program to assertion checker

Inductive invariant for gcd example:
≤+−−∧ >0∧ >0

If check fails then return a cex as a new test
u := x;v := y;w := z;
while ( x >= y ) do
if ( z > 0 )
z := z-1;
x := x+z;
else
y := y+1;
od



Given degree 2,  ≡ [1, , , , , , , 2 ,  2 ,  2 ]
Bound:  ≤ 1.9 +  −  + 0.95 + 0.24 2
After rounding:  ≤ 2 +  −  +  +  2

Requirements from assertion checker:
 Handle non-linear arithmetic
 Consume free invariants
 Produce tests as counter-examples

Micro-benchmarks: Use SGHAN’13
 Handles non-linear arithmetic, no counter-examples

Windows Device Drivers: Use Yogi (FSE’ 06)
 Cannot handle non-linear, produce counter-examples

Regression: Goldsmith et al. ‘07 , Huang et al. ’10, …

Mining specifications from tests: Dallmeier et al. `12,…

Termination: Cousot `05, ResAna, Lee et al. ’12, …

Bounds analysis: SPEED, WCET, Gulavani et al. `08, …

Invariant inference: Daikon, InvGen, Nguyen et al.`12, …

Use tests for termination proofs

Infer bounds and invariants using QP

Use off-the-shelf assertion checkers to validate

Future work: disjunctions, non-termination
a = i ; b = j ;
while(i<M || j<N)
i = i+1;
j = j+1;

Partition using predicates



<∧ ≥ ⇒ ≤−
≥∧ < ⇒ ≤−
<∧ < ⇒
≤+−−

Control flow refinement
 Sharma et al. ’11
```