Here, we list and describe the 15 new examples that we analyzed by our tool KoAT. The benchmarks can be downloaded here. To run KoAT on our benchmarks, we suggest using our web interface.
fc01.koat
This benchmark computes the Gaussian sum and thus has linear runtime complexity.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
l0(x) -> l1(f1[x | (x) <- (x)])
f1(x) -> f2(0) :|: x = 0
f1(x) -> f2(x + f1[x | (x) <- (x - 1)]) :|: x > 0
)
fc02.koat
This benchmark computes the exponential term 2^x and thus also has linear runtime complexity.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
l0(x) -> l1(f1[x | (x) <- (x)])
f1(x) -> f2(1) :|: x = 0
f1(x) -> f2(2*f1[x | (x) <- (x - 1)]) :|: x > 0
)
fc03.koat
This benchmark computes the factorial x! and also has linear runtime complexity.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
l0(x) -> l1(f1[x | (x) <- (x)])
f1(x) -> f2(1) :|: x = 0
f1(x) -> f2(x*f1[x | (x) <- (x - 1)]) :|: x > 0
)
fc04.koat
This benchmark performs a binary search and has logarithmic runtime complexity. Currently, we can only infer a linear runtime bound.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
l0(x) -> l1(f1[x | (x) <- (x)])
f1(x) -> f2(0) :|: x <= 1
f1(x) -> f2(f1[x | (x) <- (T)]) :|: 0 < T && 2*T <= x
)
fc05.koat
This benchmark has two function calls and thus an exponential runtime. It computes the Fibonacci numbers.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
l0(x) -> l1(f1[x | (x) <- (x)])
f1(x) -> f2(1) :|: x = 0
f1(x) -> f2(1) :|: x = 1
f1(x) -> f2(f1[x | (x) <- (x - 1)] + f1[x | (x) <- (x - 2)]) :|: x > 1
)
fc06.koat
This benchmark also computes the Fibonacci numbers, however, it has linear runtime complexity.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
l0(x,y,a) -> l1(x,y,f1[y | (x,y,a) <- (1,1,a)])
f1(x,y,a) -> f2(x,y,a) :|: a <= 1
f1(x,y,a) -> f2(x,f1[y | (x,y,a) <- (y,x+y,a-1)],a) :|: a > 1
)
fc07.koat
This benchmark computes the Gaussian sum and afterwards decreases this value in a second loop. Hence, it has quadratic runtime complexity. Here, we need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x a)
(RULES
l0(x,a) -> l1(f1[a | (x,a) <- (x,x)],a)
l1(x,a) -> l1(x - 1,a) :|: x > 0
f1(x,a) -> f2(x,0) :|: a = 0
f1(x,a) -> f2(x,a + f1[a | (x,a) <- (x,a - 1)]) :|: a > 0
)
fc08.koat
This benchmark computes the exponential term 2^x and afterwards it decreases this value in a second loop.
Hence, it has exponential runtime complexity.
Here, we again need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x a)
(RULES
l0(x,a) -> l1(f1[a | (x,a) <- (x,x)],a)
l1(x,a) -> l1(x - 1,a) :|: x > 0
f1(x,a) -> f2(x,1) :|: a = 0
f1(x,a) -> f2(x,2*f1[a | (x,a) <- (x,a - 1)]) :|: a > 0
)
fc09.koat
This benchmark computes the factorial x! and afterwards decreases this value in a second loop.
Hence, it has exponential runtime complexity.
Here, we again need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x a)
(RULES
l0(x,a) -> l1(f1[a | (x,a) <- (x,x)],a)
l1(x,a) -> l1(x - 1,a) :|: x > 0
f1(x,a) -> f2(x,1) :|: a = 0
f1(x,a) -> f2(x,a*f1[a | (x,a) <- (x,a - 1)]) :|: a > 0
)
fc10.koat
This benchmark computes the Gaussian sum and afterwards uses this value in a twn-loop which has logarithmic runtime complexity (see App. B). Hence, it has linear runtime complexity. Here, we need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
l0(x,y,a) -> l1(x,f1[a | (x,y,a) <- (x,y,x)],a)
l1(x,y,a) -> l2(1,y,a) :|: x <= 0
l2(x,y,a) -> l2(3*x,2*y,a) :|: x < y && x > 0
f1(x,y,a) -> f2(x,y,0) :|: a = 0
f1(x,y,a) -> f2(x,y,a + f1[a | (x,y,a) <- (x,y,a - 1)]) :|: a > 0
)
fc11.koat
This benchmark computes the exponential term 2^x and afterwards uses this value in a twn-loop which has logarithmic runtime complexity (see App. B).
Hence, it has linear runtime complexity.
Here, we need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
l0(x,y,a) -> l1(x,f1[a | (x,y,a) <- (x,y,x)],a)
l1(x,y,a) -> l2(1,y,a) :|: x <= 0
l2(x,y,a) -> l2(3*x,2*y,a) :|: x < y && x > 0
f1(x,y,a) -> f2(x,y,1) :|: a = 0
f1(x,y,a) -> f2(x,y,2*f1[a | (x,y,a) <- (x,y,a - 1)]) :|: a > 0
)
fc12.koat
This benchmark computes the factorial x! and afterwards uses this value in a twn-loop which has logarithmic runtime complexity (see App. B).
Hence, it has a runtime complexity of O(log(x!)).
Here, we need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
l0(x,y,a) -> l1(x,f1[a | (x,y,a) <- (x,y,x)],a)
l1(x,y,a) -> l2(1,y,a) :|: x <= 0
l2(x,y,a) -> l2(3*x,2*y,a) :|: x < y && x > 0
f1(x,y,a) -> f2(x,y,1) :|: a = 0
f1(x,y,a) -> f2(x,y,a*f1[a | (x,y,a) <- (x,y,a - 1)]) :|: a > 0
)
fc13.koat
This benchmark computes the sum 2^x, 2^(x - 1),..., and afterwards uses this value in a twn-loop which has logarithmic runtime complexity (see App. B).
Hence, it has quadratic runtime complexity.
Here, we need our new size bounds.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
l0(x,y,a) -> l1(x,y,a)
l1(x,y,a) -> l1(x - 1,y + f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
l1(x,y,a) -> l2(1,y,a) :|: x <= 0
l2(x,y,a) -> l2(3*x,2*y,a) :|: x < y && x > 0
f1(x,y,a) -> f2(x,y,1) :|: x = 0
f1(x,y,a) -> f2(x,y,2*f1[a | (x,y,a) <- (x,y,a - 1)]) :|: a > 0
)
fc14.koat
This benchmark corresponds to the leading example of our paper. It has an overall quadratic runtime.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y a)
(RULES
# Computes the sum x! + ... + 1! at l1 and afterwards uses this result in the second loop at l2.
l0(x,y,a) -> l1(x,y,a)
l1(x,y,a) -> l1(x-1,y+f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
l1(x,y,a) -> l2(1,y,a) :|: x <= 0
l2(x,y,a) -> l2(3*x,2*y,a) :|: x < y && x > 0
# Recursively computes the factorial a!.
f1(x,y,a) -> f2(x,y,1) :|: a = 0
f1(x,y,a) -> f2(x,y,a*f1[a | (x,y,a) <- (x,y,a - 1)]) :|: a > 0
)
fc15.koat
This benchmark performs a binary search and counts the number of iterations.
Afterwards, this counter is decreased.
Thus, this benchmark also has a logarithmic runtime complexity.
Currently, we cannot solve this benchmark since KoAT is not able to infer a finite size bound for f1[x | (x,y) <- (x,y)].
The issue arises because the update of the last transition does not conform to the local size bound template in Equation (1) of our paper, as it involves temporary variables.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y)
(RULES
l0(x,y) -> l1(f1[x | (x,y) <- (x,y)],y)
l1(x,y) -> l1(x - 1,y) :|: x > 0
f1(x,y) -> f2(0,y) :|: y <= 1
f1(x,y) -> f2(x + 1,f1[x | (x,y) <- (x,T)]) :|: 0 < T && 2*T <= y
)