AProVE's Web Interface

A custom version of AProVE which only proves termination of C and LLVM programs.
Experimental Evaluation of "Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution"
Additional Information about this Version of AProVE

Pick the language of your input below. On the next page you can paste your program, upload a file, or load a preset example, and then let AProVE run on our servers. No installation is required. If you would rather run AProVE on your own machine, see the Get AProVE page.

Frontend Languages

Languages that programs are actually written in. AProVE translates them into rewrite systems internally.


Backend Languages

Analysis-oriented formalisms such as term rewrite systems and integer transition systems, which can also be given directly as input.

C (termination)
LLVM (termination)
C (complexity)
LLVM (complexity)

Details on every input format, including syntax help pages, are collected on the Usage page.