llvm2KITTeL is a converter from LLVM's intermediate representation into a format that can be handled by the automatic termination prover KITTeL.
This is an adapted version of llvm2KITTeL which handles OpenCL and CUDA
kernels. The bitcode for these kernels should be produced by
GPUVerify with
GPUVerify's --stop-at-opt option.
Stephan Falke, Jeroen Ketema, Marc Brockschmidt
The OpenCL and CUDA related changes are by Jeroen Ketema.
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