KoAT

Short description of KoAT.

What inputs are supported?

The following input formats are supported:

• Integer Transition Systems (ITS)
• Probabilistic ITS
• C Integer

What properties can be verified?

Termination, (upper) complexity bounds, positive almost-sure termination, (upper) bounds on expected complexity.

What are the tool’s main techniques for the supported (input, property) pairs?

Modular approach based on time and size bound computations, ranking functions, complete techniques for termination/complexity analysis, control-flow refinement, ...

What external tools are used? (e.g., compilers, SMT solvers)

A detailed and complete description of external tools can be found here.

• SMT solver: Z3
• Invariants: APRON
• Control-flow refinement: iRankFinder
• Algebraic Numbers: SymPy
• Transforming C-Code to ITS: Clang and llvm2kittel

What is the tool’s URL?

https://koat.verify.rwth-aachen.de/

KoAT can be used via a web interface, via a static binary, or its Docker image.

Example(s)

For an exhaustive example collection, consider the Termination Problem DataBase with thousands of example inputs for the supported languages for termination and complexity. Additionally, the web interface provides examples.

References

The publications on KoAT can be found here.