Java Program Analysis by Symbolic Execution

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 dy-namic dispatch, complex object hierarchies, or side-effects with far-reaching consequences involving the global heap. In this thesis, we present a preprocessing step for Java Bytecode 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 havin