llvm2KITTeL

llvm2KITTeL is a converter from LLVM's intermediate representation into a format that can be handled by the automatic termination prover KITTeL.

Author

Stephan Falke, Jeroen Ketema, Marc Brockschmidt

Papers

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