tr-announce

Download

tr-announce@lists.rwth-aachen.de

September 2011

1 participants
1 discussions

2011-19: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
by Carsten Fuhs 12 Sep '11

12 Sep '11

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.

1 0