*Result*: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode ⋆
Title:
Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode ⋆
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Collection:
CiteSeerX
Document Type:
*Academic Journal*
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.4FCC20C7
Database:
BASE
*Further Information*
*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*