A static ELF binary, containing all necessary dependencies, can be downloaded here.
Please make sure that the binary is executable by running chmod +x koat2_static.
For older releases of KoAT, in order to apply the control-flow refinement technique presented here, the tool iRankFinder
(resp. the module pyRankFinder) is required.We recommend using the pre-compiled version irankfinder_v1.3.1_rhel7.zip. Please ensure that your PATH environment variable contains the path to the unzipped folder irankfinder, to its subfolder partialevaluation/bin, and to its subfolder ppl.
In order to apply our novel size bound techniques, SymPy (see here) must be installed.
KoAT2 can then be run on an example by executing
/PATH/TO/KOAT2/koat2_static analyse -i /PATH/TO/EXAMPLES/myExample.koat
Note that the static binary only accepts integer programs as input. C programs have to be translated to integer programs using Clang and llvm2kittel.
Similar to the Docker image, you can use the flags to determine the method for computing local runtime bounds, to determine the depth of MΦRFs, and to decide whether control-flow refinement via partial evaluation should be used.
For older releases of KoAT,
the latter requires that the path to iRankFinder is contained in the PATH environment variable, as described above.
Additional Flags
Both the Docker image and the static binary can be invoked with additional flags, e.g., for choosing only certain preprocessors, for choosing a different output format, for getting more details on the computation process, and many more. To see a detailed description of these flags, run
docker run koat2:latest its analyse --help
when using the Docker image or
/PATH/TO/KOAT/koat2_static analyse --help
when using the static binary.
Note that docker run koat2:latest c analyse --help will list all flags of Clang, as Clang is invoked first to translate a C program into LLVM code.
For instance, to obtain the automatically generated proof of KoAT instead of just the result of the analysis, one has to add the flag -r all. To obtain the output in the format of the Termination and Complexity Competition, one has to add the flag -r termcomp.
If KoAT2 should analyze a probabilistic program, please use the subcommand prob-analyse.
/PATH/TO/KOAT/koat2_static prob-analyse --help