tr-announce September 2011

tr-announce@lists.rwth-aachen.de

1 Teilnehmer
1 Diskussionen

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

von 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.

12 Jahre, 7 Monate

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