KITTeL is an automatic termination prover for integer transition systems and imperative programs written in a fragment of Simple. For programs written in other languages (e.g., C), consider using the frontend llvm2KITTeL.
KoAT is an automatic complexity analyzer taking the same kinds of inputs.
Stephan Falke, Marc Brockschmidt
Stephan Falke, Deepak Kapur, Carsten Sinz: Termination Analysis of C Programs Using Compiler Intermediate Languages. RTA 2011: 41-50
Stephan Falke, Deepak Kapur, Carsten Sinz: Termination Analysis of Imperative Programs Using Bitvector Arithmetic. VSTTE 2012: 261-277
Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl: Alternating Runtime and Size Complexity Analysis of Integer Programs. TACAS 2014: 140-155