AProVE

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 (complexity)

Accepted file formats: llvm

Version bitvectors
Disclaimer