This page contains additional information on our article “AProVE (KoAT + LoAT)” for the SV-Comp 2025. The most recent version of our framework can be found here.

Implementation

AProVE is implemented in Java 17 and needs a JRE to be executed. See the README of the Zenodo archive for more information about the dependencies of AProVE (KoAT + LoAT).

Invocation:

AProVE (KoAT + LoAT) can be invoked for C files using the following call pattern (depending on the bit-width used in the task):

./AProVE.sh --bit-width 32 problemFile or ./AProVE.sh --bit-width 64 problemFile

Here, problemFile is the path to the C file to be analyzed for termination of the function main(). AProVE’s proof of termination (or its failed proof attempt) is output on stdout.

Leading Examples

In the following, we provide the examples of the paper as C programs:

C Version of Loop (1):

extern int __VERIFIER_nondet_int(void);

int main() {
  int x = __VERIFIER_nondet_int();
  int y = __VERIFIER_nondet_int();
  int z = __VERIFIER_nondet_int();

  while(y - x*x > 0 && x > 0) {
    x = 4*x;
    y = 9*y - 8*z*z*z;
  }
  return 0;
}

C Version of the non-terminating Loop (1):

extern int __VERIFIER_nondet_int(void);

int main() {
  int x = __VERIFIER_nondet_int();
  int y = __VERIFIER_nondet_int();
  int z = __VERIFIER_nondet_int();

  while(y - x*x > 0) {
    x = 4*x;
    y = 9*y - 8*z*z*z;
  }
  return 0;
}

C Version of the linear version of Loop (1):

extern int __VERIFIER_nondet_int(void);

int main() {
  int x = __VERIFIER_nondet_int();
  int y = __VERIFIER_nondet_int();

  while(x < y && x > 0) {
    x = 3*x;
    y = 2*y;
  }
  return 0;
}

C Version of the non-terminating, linear version of Loop (1):

extern int __VERIFIER_nondet_int(void);

int main() {
  int x = __VERIFIER_nondet_int();
  int y = __VERIFIER_nondet_int();

  while(x < y) {
    x = 3*x;
    y = 2*y;
  }
  return 0;
}