@TechReport{HenselEtAl16,
  author      = "Jera Hensel and J\"urgen Giesl and Florian Frohn and Thomas Str\"oder",
  title       = "Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution",
  institution = "RWTH Aachen",
  keywords    = "termination analysis, bitvectors, C programs, LLVM",
  year        = "2016",
  number      = "AIB-2016-04",
  month       = "April",
  url         = "http://aib.informatik.rwth-aachen.de/2016/2016-04.pdf"
}