Treffer: Supervised by

This master thesis is based on B2BPL, a translator from BML annotated Java Bytecode to BoogiePL conceived and implemented in previous work at ETH Zurich. We are primarily interested in extending the existing translator with some more elaborate mechanisms in terms of translating method invocations and invariant checks. Although B2BPL is doing fine in translating annotated Bytecode programs already, there is still room for improvement. We are also keen to see B2BPL integrated in a broader verification environment, where Java Bytecode can be directly translated to BoogiePL and verified by Boogie in an integrated development environment like Eclipse. In order to achieve these goals, we roll up the existing implementation of the method call translation algorithm and introduce a mechanism to perform simple but more flexible invariant checks (with a particular focus on method calls). The translation of method calls is improved by using the Boogie-specific call command while at the same time, exception handling is extended with an additional level of flexibility. Furthermore, invariant checks are refined such that only the invariants of modified objects need to be checked, and that inadmissible invariants are ruled out automatically. In addition to these modification in