AProVE 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

Analysis of LLVM (termination)

LLVM code. Show Help (in new window)

Enter Program Code
Upload a File

Choose file

Accepted file formats: llvm

Upload a File or Text?

Timeout (1 seconds minimum, 300 seconds maximum):

Output format:

HTML

Plain Text

Version bitvectors