Web Interface

Analyze an Integer Program with KoAT right here. The input format is described here.

Program
Examples
Analysis
Result

Proof

Running KoAT Locally

The behaviour of the interface above can be reproduced via

See Getting Started for the Docker image and the static binary, and Documentation for the remaining flags.

Other Interfaces

The interface above analyzes integer programs. For probabilistic integer programs and for C programs, use the interfaces hosted with our tool AProVE: a web interface for probabilistic integer programs and a web interface for C programs. The legacy AProVE interface for integer programs is superseded by the interface on this page and is kept only for reference; it runs an older KoAT.