The source code of our newest version of KoAT be found here. The most recent official version of KoAT is also available on GitHub. See here for a list of external tools and libraries used by KoAT.
Our implementation can be executed via the web interfaces, via a Docker image, and via the provided static binary.
Concerning the input format, for integer programs we use the corresponding input format from the Termination and Complexity Competition as described here, which is extended by probabilistic choices. Note that a disjunction is modeled by two parallel transitions with the same update, and negations are modeled by flipping every comparator (i.e., ¬(x<y) is equivalent to x≥y).
For C programs, we also use the corresponding input format from the Termination and Complexity Competition as described here. To analyze C programs, KoAT translates them into its format for integer programs using Clang and llvm2kittel.