The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Java Program Analysis by Symbolic Execution
Carsten Otto
AIB 2013-16
Program analysis has a long history in computer science. Even when only
considering the important aspect of termination analysis, in the past
decades an overwhelming number of different techniques has been
developed. While the programming languages considered by these
approaches initially were more of theoretical importance than of
practical use, recently also automated analyses for imperative
programming languages like C or Java have been developed. Here, a major
challenge is to deal with language constructs and concepts which do not
exist in simpler languages. For example, in Java one often uses dynamic
dispatch, complex object hierarchies, or side-effects with far-reaching
consequences involving the global heap.
In this thesis, we present a preprocessing step for JBC programs in
which all such complicated language constructs are handled. This way,
subsequent analyses do not need to be concerned with these, and making
use of existing techniques is easy. In particular, we show how Symbolic
Execution Graphs can be constructed which contain an over-approximation
of all possible program runs. This way, and by taking care of having a
precise approximation, the information contained in the constructed
graphs can, for example, be used to reason about the termination
behavior of the original program.
Additionally to the construction of such graphs, in this thesis we
present a new analysis technique which helps end users identify parts of
the analyzed code which are irrelevant for the desired outcome. This
way, programming errors causing code to be not executed can be
identified and, consequently, fixed by the user. For this technique to
be useful, the information contained in the previously constructed graph
needs to be precise. We will demonstrate that this is the case.
For the techniques presented in this thesis, a rigorous formalization is
shown. To comply with the overall goal of, for example, automated
termination analysis, we also need to implement the techniques and
theoretical results. In this thesis we show how certain hard to automate
aspects can be approached, leading to a competitive implementation.
The techniques presented in this thesis are implemented in the AProVE
tool. As also related techniques working on Symbolic Execution Graphs
are implemented in AProVE, with the click of a button users can analyze
JBC programs for (non)termination and find irrelevant code. In the
annual International Termination Competition, it is demonstrated that
currently AProVE is the most powerful termination analyzer for JBC programs.
