Here, we list and describe the 45 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. C of the long version of our paper). 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. C). 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. C). 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. C). 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
)

fc16.koat

This benchmark contains a simple loop represented recursively by two consecutive transitions and it also includes non-determinism.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS l1_ret f2))
(VAR x y a)
(RULES
  l0(x,y,a) -> l1(x,y,a)
  l1(x,y,a) -> l1'(x,y + T,a) :|: x > 0
  l1'(x,y,a) -> l1_ret(x,y + l1[y | (x,y,a) <- (x - 1,y,a)],a) :|: x > 0
)

fc17.koat

This benchmark is similar to fc13.koat and computes the sum 2^x, 2^(x - 1),.... However, here recursion is used instead of a loop. Thus, this benchmark contains nested function calls.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS l1_ret f2))
(VAR x y a)
(RULES
  l0(x,y,a) -> l1(x,y,a)
  l1(x,y,a) -> l1'(x,y + f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
  l1'(x,y,a) -> l1_ret(x,y + l1[y | (x,y,a) <- (x - 1,y,a)],a) :|: 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
)

fc18.koat

This benchmark is similar to the leading example of our paper (i.e., fc14.koat). However, here recursion is used instead of a loop for the summation of the factorials x!, (x - 1)!,... and we omitted the twn-loop. The benchmark has an overall quadratic runtime.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS l1_ret f2))
(VAR x y a)
(RULES
  # Computes the sum x! + ... + 1! at l1.
  l0(x,y,a) -> l1(x,y,a)
  l1(x,y,a) -> l1'(x,y+f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
  l1'(x,y,a) -> l1_ret(x,y + l1[y | (x,y,a) <- (x - 1,y,a)],a) :|: 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
)

fc19.koat

This benchmark is similar to fc17.koat and computes the sum 2^x, 2^(x - 1),.... Thus, this benchmarks also contains nested function calls. Afterwards, this value is used in a twn-loop which has logarithmic runtime complexity (see App. C). Hence, it has quadratic runtime complexity. Here, we need our new size bounds.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS l1_ret f2))
(VAR x y a)
(RULES
  l0(x,y,a) -> l1(x,y,a)
  l1(x,y,a) -> l1'(x,y + f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
  l1'(x,y,a) -> l1_ret(x,y + l1[y | (x,y,a) <- (x - 1,y,a)],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
)

fc20.koat

This benchmark is similar to the leading example of our paper (i.e., fc14.koat). However, here recursion is used instead of a loop for the summation of the factorials x!, (x - 1)!,.... The benchmark has an overall quadratic runtime.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS l1_ret 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,y+f1[a | (x,y,a) <- (x,y,x)],a) :|: x > 0
  l1'(x,y,a) -> l1_ret(x,y + l1[y | (x,y,a) <- (x - 1,y,a)],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
)

Additional Benchmarks to Demonstrate KoAT’s Limitations and the use of Amortized Costs

fc21.koat

This benchmark implements a simple recursive loop which has logarithmic runtime (x grows exponentially faster than y). However, this loop does not admit a linear (multiphase) ranking function.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y)
(RULES
  l0(x,y) -> l1(f1[x | (x,y) <- (x,y)],y)
  f1(x,y) -> f2(x,y) :|: x <= 0
  f1(x,y) -> f2(x,y) :|: y <= x
  f1(x,y) -> f2(f1[x | (x,y) <- (3*x,2*y)],y) :|: 0 < x && x < y
)

fc22.koat

This benchmark implements the naive prime number test with runtime sqrt(x) for a number x. Currently, we cannot handle this loop due to non-linear guards in the recursive calls. If one over-approximates the guard n*n <= x by n <= x, then we are able to infer linear runtime complexity. Furthermore, if one considers the tail-recursive variant of this program, then we are also able to infer a linear runtime bound. The reason is that we have more support for non-linear updates and guards in the classical setting.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x n)
(RULES
  l0(x,n) -> l1(f1[x | (x,n) <- (x,1)],n) :|: x > 0
  f1(x,n) -> f2(n,n) :|: T*n = x && T > 0 # n divides x
  f1(x,n) -> f2(0,n) :|: n*n <= x         # x is prime
  f1(x,n) -> f2(f1[x | (x,n) <- (x, n + 1)],n) :|: n*n <= x
)

fc23.koat

The following program represents a dynamic array whose size is doubled when the array is full. Here, a represents the current size of the array, x is the number of elements in the array, and y is the total number of elements that should be inserted into the array. The third transition, which copies the elements of the array, has cost a. This is denoted by {a}. Amortized complexity analysis yields constant runtime for this transition and thus linear complexity for the overall program. KoAT is also able to infer linear runtime complexity by “normalizing” the costs.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR x y a)
(RULES
  l0(x,y,a) -> l1(1,y,1)
  l1(x,y,a) -> l1(x+1,y - 1,a) :|: x != a && y > 0
  l1(x,y,a) -{a}> l1(x + 1,y - 1,2*a) :|: x = a && y > 0
)

fc24.koat

The following program shows KoATs limitations regarding invariant generation for recursive programs. The program has a recursive loop (the third transition) which decreases x by y. Currently, KoAT is not able to propagate the invariant y > 0 to recursive subprograms. In the future, we will try to lift that approach from the classical setting to recursive programs.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y)
(RULES
  l0(x,y) -> l1(f1[x | (x,y) <- (x,y)],y) :|: y > 0
  f1(x,y) -> f2(x,y) :|: x <= 0
  f1(x,y) -> f2(f1[x | (x,y) <- (x - y,y)],y) :|: 0 < x
)

fc25.koat

Currently, KoAT only infers octagon domain invariants (i.e., inequations of the form x ± y ≤ c for variables x and y, and a constant c) via Apron. The following benchmark needs stronger (polyhedron) invariants. More precisely, to infer a complexity bound for the loop, one has to observe that c + b - a > 0 and thus c > 0 holds.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR a b c d)
(RULES
  l0(a,b,c,d) -> l1(a,b,c+a-b,d) :|: a > b && C > 0
  l1(a,b,c,d) -> l1(a,b,c,d-c) :|: d > 0
)

New Benchmarks derived from the TermComp

fc26.koat

This benchmark is based on the C program from the TermComp which computes the relation x <= y.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS le_ret))
(VAR x y r)
(RULES
  main(x,y,r) -> l1(x,y,le[r | (x,y,r) <- (x,y,r)]) :|: x > 0 && y > 0
  le(x,y,r) -> le_ret(x,y,le[r | (x,y,r) <- (x - 1,y - 1,r)]) :|: x > 0 && y > 0
  le(x,y,r) -> le_ret(x,y,1) :|: x = 0
)

fc27.koat

This benchmark is a simplified version of the C program from the TermComp which computes the number of ways to write a number p as a sum of integers ≤ q.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS parts_ret))
(VAR p q r)
(RULES
  main(p,q,r) -> l1(p,q,parts[r | (p,q,r) <- (p,q,r)])
  parts(p,q,r) -> parts_ret(p,q,1) :|: p <= 0
  parts(p,q,r) -> parts_ret(p,q,parts[r | (p,q,r) <- (p - q,q,r)] + parts[r | (p,q,r) <- (p,q - 1,r)]) :|: q > 0 && q <= p
)

fc28.koat

This benchmark is based on the C program from the TermComp which computes the number of ways to write a number p as a sum of integers ≤ q.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS parts_ret))
(VAR p q r)
(RULES
  main(p,q,r) -> l1(p,q,parts[r | (p,q,r) <- (p,q,r)])
  parts(p,q,r) -> parts_ret(p,q,1) :|: p <= 0
  parts(p,q,r) -> parts_ret(p,q,parts[r | (p,q,r) <- (p,p,r)]) :|: q > p
  parts(p,q,r) -> parts_ret(p,q,parts[r | (p,q,r) <- (p - q,q,r)] + parts[r | (p,q,r) <- (p,q - 1,r)]) :|: q > 0 && q <= p
)

fc29.koat

This benchmark is also based on a C program from the TermComp.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS rec_ret))
(VAR a r rH)
(RULES
  main(a,r,rH) -> l1(a,rec[r | (a,r,rH) <- (a,r,rH)],rH)
  rec(a,r,rH) -> rec_ret(0,r,rH) :|: a = 0
  rec(a,r,rH) -> rec_h1(a,rec[r | (a,r,rH) <- (a - 1,r,rH)],rH) :|: a > 0
  rec_h1(a,r,rH) -> rec_h2(a,r,r) :|: a > 0
  rec_h2(a,r,rH) -> rec_ret(a,r + 1, rH)
)

fc30.koat

This benchmarks extends the previous example by a consecutive loop which decreases the value of the function call.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS rec_ret))
(VAR a r rH)
(RULES
  main(a,r,rH) -> l1(a,rec[r | (a,r,rH) <- (a,r,rH)],rH)
  rec(a,r,rH) -> rec_ret(0,r,rH) :|: a = 0
  rec(a,r,rH) -> rec_h1(a,rec[r | (a,r,rH) <- (a - 1,r,rH)],rH) :|: a > 0
  rec_h1(a,r,rH) -> rec_h2(a,r,r) :|: a > 0
  rec_h2(a,r,rH) -> rec_ret(a,r + 1, rH)
  l1(a,r,rH) -> l1(a,r - 1,rH) :|: r > 0
)

fc31.koat

This benchmark is based on the C program from the TermComp which computes the length of a string.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS strlen_rec_ret))
(VAR p end)
(RULES
  main(p,end) -> main_ret(strlen_rec[p | (p,end) <- (0,end)],end)
  strlen_rec(p,end) -> strlen_rec_ret(0,end) :|: p = end
  strlen_rec(p,end) -> strlen_rec_ret(1 + strlen_rec[p | (p,end) <- (p + 1,end)],end) :|: p < end
)

fc32.koat

This benchmark is based on the C program from the TermComp which computes a simple loop recursively. However, to infer a finite complexity bound, a suitable invariant must be inferred.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS main))
(RETURNLOCATIONS (FUNCTIONSYMBOLS twoWay_ret))
(VAR x y r)
(RULES
  main(x,y,r) -> l1(x,y,twoWay[r | (x,y,r) <- (x,y,r)]) :|: x = 1
  twoWay(x,y,r) -> twoWay_ret(x,y,y*twoWay[r | (x,y,r) <- (x,y - 1,r)]) :|: x = 1 && y > 0
  twoWay(x,y,r) -> twoWay_ret(x,y,y*twoWay[r | (x,y,r) <- (x,y + 1,r)]) :|: x = 0 && y > 0
  twoWay(x,y,r) -> twoWay_ret(x,y,1) :|: y < 0
)

fc33.koat

This benchmark is a simplified version of the C program from the TermComp which computes the binomial coefficient recursively.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR n k a)
(RULES
  l0(n,k,a) -> l1(f1[a | (n,k,a) <- (n,k,n)],f1[a | (n,k,a) <- (n,k,k)]*f1[a | (n,k,a) <- (n,k,n-k)],a)
  f1(n,k,a) -> f2(n,k,1) :|: a = 0
  f1(n,k,a) -> f2(n,k,a*f1[a | (n,k,a) <- (n,k,a - 1)]) :|: a > 0
)

fc34.koat

This benchmark now corresponds to the C program from the TermComp which computes the binomial coefficient recursively.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y n k r1 r2 r3 a)
(RULES
  l0(x,y,n,k,r1,r2,r3,a) -> l1(x,y,0,k,r1,r2,r3,a)
  l1(x,y,n,k,r1,r2,r3,a) -> l2(x,y,n + 1,0,r1,r2,r3,a) :|: n <= x
  l2(x,y,n,k,r1,r2,r3,a) -> l2(x,y,n,k + 1,f1[a | (x,y,n,k,r1,r2,r3,a) <- (x,y,n,k,r1,r2,r3,n)],f1[a | (x,y,n,k,r1,r2,r3,a) <- (x,y,n,k,r1,r2,r3,k)],f1[a | (x,y,n,k,r1,r2,r3,a) <- (x,y,n,k,r1,r2,r3,n - k)],a) :|: k <= x
  l2(x,y,n,k,r1,r2,r3,a) -> l1(x,y,n,k,r1,r2,r3,a)
  f1(x,y,n,k,r1,r2,r3,a) -> f2(x,y,n,k,r1,r2,r3,1) :|: a = 0
  f1(x,y,n,k,r1,r2,r3,a) -> f2(x,y,n,k,r1,r2,r3,a*f1[a | (x,y,n,k,r1,r2,r3,a) <- (x,y,n,k,r1,r2,r3,a - 1)]) :|: a > 0
)

fc35.koat

This benchmark is a harder version of the previous benchmark since it contains a non-linear combination of function calls.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x y n k r1 r2 a)
(RULES
  l0(x,y,n,k,r1,r2,a) -> l1(x,y,0,k,r1,r2,a)
  l1(x,y,n,k,r1,r2,a) -> l2(x,y,n + 1,0,r1,r2,a) :|: n <= x
  l2(x,y,n,k,r1,r2,a) -> l2(x,y,n,k + 1,f1[a | (x,y,n,k,r1,r2,a) <- (x,y,n,k,r1,r2,n)],f1[a | (x,y,n,k,r1,r2,a) <- (x,y,n,k,r1,r2,k)]*f1[a | (x,y,n,k,r1,r2,a) <- (x,y,n,k,r1,r2,n - k)],a) :|: k <= x
  l2(x,y,n,k,r1,r2,a) -> l1(x,y,n,k,r1,r2,a)
  f1(x,y,n,k,r1,r2,a) -> f2(x,y,n,k,r1,r2,1) :|: a = 0
  f1(x,y,n,k,r1,r2,a) -> f2(x,y,n,k,r1,r2,a*f1[a | (x,y,n,k,r1,r2,a) <- (x,y,n,k,r1,r2,a - 1)]) :|: a > 0
)

New Benchmarks derived from the SV-Comp

fc36.koat

This benchmark is based on the C program from the SV-Comp which computes the optimal number of steps needed to solve the classic Towers of Hanoi puzzle.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
  l0(x) -> l1(f1[x | (x) <- (x)])
  f1(x) -> f2(1) :|: x = 1
  f1(x) -> f2(2*f1[x | (x) <- (x - 1)] + 1) :|: x > 0
)

fc37.koat

This benchmark extends the previous example by introducing a loop that uses the number of steps required to solve the Towers of Hanoi puzzle as a size bound.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS f2))
(VAR x)
(RULES
  l0(x) -> l1(f1[x | (x) <- (x)])
  l1(x) -> l1(x - 1) :|: x > 0

  f1(x) -> f2(1) :|: x = 1
  f1(x) -> f2(2*f1[x | (x) <- (x - 1)] + 1) :|: x > 0
)

fc38.koat

This benchmark is a simplified version of the C program from the SV-Comp which implements a recursive function to determine whether a given integer is even or odd.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS odd_ret))
(VAR x)
(RULES
  l0(x) -> l1(odd[x | (x) <- (x)])

  odd(x) -> odd_ret(1) :|: x = 0
  odd(x) -> odd_ret(0) :|: x = 1
  odd(x) -> odd_ret(odd[x | (x) <- (x - 2)]) :|: x > 1
)

fc39.koat

This benchmark is a variant of the C program from the SV-Comp which implements mutually recursive functions for even/odd checking.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS odd_ret even_ret))
(VAR x)
(RULES
  l0(x) -> l1(odd[x | (x) <- (x)])

  odd(x) -> odd_ret(1) :|: x = 0
  odd(x) -> odd_ret(0) :|: x = 1
  odd(x) -> odd_ret(even[x | (x) <- (x - 1)]) :|: x > 1

  even(x) -> even_ret(0) :|: x = 0
  even(x) -> even_ret(1) :|: x = 1
  even(x) -> even_ret(odd[x | (x) <- (x - 1)]) :|: x > 1
)

fc40.koat

This benchmark is based on the C program from the SV-Comp which computes the greatest common divisor (GCD) of two integers.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS gcd_ret))
(VAR x y r)
(RULES
  l0(x,y,r) -> l1(x,y,gcd[r | (x,y,r) <- (x,y,r)])

  gcd(x,y,r) -> gcd_ret(x,y,0) :|: x <= 0
  gcd(x,y,r) -> gcd_ret(x,y,0) :|: y <= 0
  gcd(x,y,r) -> gcd_ret(x,y,x) :|: x = y
  gcd(x,y,r) -> gcd_ret(x,y,gcd[r | (x,y,r) <- (x - y,y,r)]) :|: x > y && y > 0
  gcd(x,y,r) -> gcd_ret(x,y,gcd[r | (x,y,r) <- (x,y - x,r)]) :|: x < y && x > 0
)

fc41.koat

This benchmark extends the previous example by adding a counter to the C program that computes the GCD of two integers.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS gcd_ret))
(VAR x y r)
(RULES
  l0(x,y,r) -> l1(x,y,gcd[r | (x,y,r) <- (x,y,r)])
  l1(x,y,r) -> l1(x,y,r - 1) :|: r > 0

  gcd(x,y,r) -> gcd_ret(x,y,0) :|: x <= 0
  gcd(x,y,r) -> gcd_ret(x,y,0) :|: y <= 0
  gcd(x,y,r) -> gcd_ret(x,y,x) :|: x = y && x > 0 && y > 0
  gcd(x,y,r) -> gcd_ret(x,y,gcd[r | (x,y,r) <- (x - y,y,r)]) :|: x > y && y > 0
  gcd(x,y,r) -> gcd_ret(x,y,gcd[r | (x,y,r) <- (x,y - x,r)]) :|: x < y && x > 0
)

fc42.koat

This benchmark is based on the C program from the SV-Comp which computes the product of two integers using a recursive algorithm.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS mul_ret))
(VAR x y r)
(RULES
  l0(x,y,r) -> l1(x,y,mul[r | (x,y,r) <- (x,y,r)]) :|: x >= 0 && y >= 0

  mul(x,y,r) -> mul_ret(x,y,0) :|: y = 0
  mul(x,y,r) -> mul_ret(x,y,x + mul[r | (x,y,r) <- (x,y - 1,r)]) :|: y > 0
)

fc43.koat

This benchmark extends the previous C program (which computes multiplication via a recursive algorithm) by adding a loop-based counter.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS mul_ret))
(VAR x y r)
(RULES
  l0(x,y,r) -> l1(x,y,mul[r | (x,y,r) <- (x,y,r)]) :|: x >= 0 && y >= 0
  l1(x,y,r) -> l1(x,y,r - 1) :|: r > 0

  mul(x,y,r) -> mul_ret(x,y,0) :|: y = 0
  mul(x,y,r) -> mul_ret(x,y,x + mul[r | (x,y,r) <- (x,y - 1,r)]) :|: y > 0
)

fc44.koat

This benchmark is based on the C program from the SV-Comp which implements insertion sort recursively.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS insS_ret))
(VAR x y r)
(RULES
  l0(x,y,s,r) -> l1(x,y,s,insS[r | (x,y,s,r) <- (0,y,s,r)])

  insS(x,y,s,r) -> insS_ret(x,y,s,r) :|: x = s
  insS(x,y,s,r) -> insS'(x,x,s,r) :|: x < s
  insS'(x,y,s,r) -> insS'(x,y - 1,s,r) :|: y > 0
  insS'(x,y,s,r) -> insS_ret(x,y,s,insS[r | (x,y,s,r) <- (x + 1,y,s,r)]) :|: y = 0 && x < s
)

fc45.koat

This benchmark is based on the C program from the SV-Comp which implements selection sort recursively.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(RETURNLOCATIONS (FUNCTIONSYMBOLS selS_ret))
(VAR x y r)
(RULES
  l0(x,y,s,r) -> l1(x,y,s,selS[r | (x,y,s,r) <- (0,y,s,r)])

  selS(x,y,s,r) -> selS_ret(x,y,s,r) :|: x = s
  selS(x,y,s,r) -> selS'(x,x + 1,s,r) :|: x < s
  selS'(x,y,s,r) -> selS'(x,y + 1,s,r) :|: y < s
  selS'(x,y,s,r) -> selS_ret(x,y,s,selS[r | (x,y,s,r) <- (x + 1,y,s,r)]) :|: y = 0 && x < s
)