The following technical report is available from http://aib.informatik.rwth-aachen.de:
Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode Marc Brockschmidt, Thomas Ströder, Carsten Otto, Jürgen Giesl AIB 2011-19
Recently, we developed an approach for automated termination proofs of Java Bytecode (JBC), which is based on constructing and analyzing termination graphs. These graphs represent all possible program executions in a finite way. In this paper, we show that this approach can also be used to detect non-termination or NullPointerExceptions. Our approach automatically generates witnesses, i.e., calling the program with these witness arguments indeed leads to non-termination resp. to a NullPointerException. Thus, we never obtain "false positives". We implemented our results in the termination prover AProVE and provide experimental evidence for the power of our approach.