Our implementation can be tested via a web interface for integer programs, a web interface for probabilistic integer programs, and a web interface for C programs. These web interfaces are provided via special versions of the web site of our tool AProVE.
- The window
Enter Program Codeshows the program that is currently analyzed. The user can modify the program or replace it by a new one. - In addition, one can also
Upload a Fileof a program to analyze (where the file should have the extension.koatresp. the extension.c). - To run KoAT, one can select which local bound computation method should be applied (MΦRFs where the depth has to be limited or the twn-technique), one can decide whether control-flow refinement should be used, and one can choose the timeout. Afterwards, the button
Submitcalls KoAT. - In the proof output of KoAT, clicking on
Show Graphshows the graph of the program where the currently analyzed program part is highlighted in color. For the current MΦRF, the decreasing transitions are colored in red and the remaining non-increasing transitions are colored in blue. - After viewing the result of KoAT,
Return to program inputtakes you back to the web page with the input program.