Reference:

Dejvuth Suwimonteerabuth. Verifying Java bytecode with the Moped model checker. Master's thesis, Universität Stuttgart, 2004.

Abstract:

In recent years, model checking algorithms of infinite-state systems have been extensively studied and various tools have been developed. Moped – a model checker for pushdown systems, has been developed by S. Schwoon. The tool acts as a combined linear-time temporal logic (LTL) and reachability model checker. The result lightens up a way of the automatic software verification. Nevertheless, a gap still exists between the input model of Moped and programming languages which are normally used nowadays.

The thesis investigates an approach to close the gap and verify the correctness of Java programs. The compiled version of Java source code, namely Java bytecode, are of the interest, since it is restricted to a set of basic statements, and therefore causes the program analysis much simpler. The thesis studies the nature of Java bytecodes, and gives algorithms for translating them into pushdown systems. A translator tool has been implemented to support the concepts. The integration of the translator and Moped thus enables `fully' automatic verification.

Experimental studies show that the approach can be used to verify properties of rather complicated algorithms. Examples discussed throughout the thesis demonstrate powers of the tool, including recursive calls, object manipulations, inheritances, and exception handlings.

Suggested BibTeX entry:

@mastersthesis{Suw04,
    author = {Dejvuth Suwimonteerabuth},
    school = {Universit{\"a}t Stuttgart},
    title = {Verifying {Java} Bytecode with the {Moped} Model Checker},
    year = {2004}
}