AIB 2016-04: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

[Jera Hensel]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Proving Termination of Programs with Bitvector Arithmetic by Symbolic
Execution
Jera Hensel, Jürgen Giesl, Florian Frohn, and Thomas Ströder
AIB 2016-04

In earlier work, we developed an approach for automated termination
analysis of C programs with explicit pointer arithmetic, which is based
on symbolic execution. However, similar to many other termination
techniques, this approach assumed the program variables to range over
mathematical integers instead of bitvectors. This eases mathematical
reasoning but is unsound in general. In this paper, we extend our
approach in order to handle fixed-width bitvector integers. Thus, we
present the first technique for termination analysis of C programs that
covers both byte-accurate pointer arithmetic and bit-precise modeling of
integers. We implemented our approach in the automated termination
prover AProVE and evaluate its power by extensive experiments.