tr-announce September 2011

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2011-19: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode

by Carsten Fuhs

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.

13 years

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce September 2011