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

C programming language. Show Help (in new window)

Accepted file formats: c

Version bitvectors
Disclaimer