Java Virtual Machine using graph grammars

dr. P.M. van den Broek dr. ir. A. Rensink Summary Model checking is used to find problems in software. However the run-time behaviour of a program is poorly covered by existing model checking. To be able to analyse this run-time behaviour we want to be able to translate a Java program into graph grammars. This report especially focuses on the translation of Java byte code into graph grammars. To be able to do this translation, a run-time state of a program has to be represented in a graph. For this representation a Meta model is developed. A translator has been designed and implemented to create graphs and graph production rules corresponding to this Meta model. Using this translator simple Java programs can be translated to graph grammars. Currently not all JVM instructions and Java concepts are implemented; this is planned for the future. The templates used for the translation are very complex and need to be systematically designed in the future. This translator can contribute to better software analysis and in the end help to find more bugs.