Formal Translation of Bytecode into BoogiePL

13 years 4 months ago

Download people.inf.ethz.ch

Many modern program veriﬁers translate the program to be veriﬁed and its speciﬁcation into a simple intermediate representation and then compute veriﬁcation conditions on this representation. Using an intermediate language improves the interoperability of tools and facilitates the computation of small veriﬁcation conditions. Even though the translation into an intermediate representation is critical for the soundness of a veriﬁer, this step has not been formally veriﬁed. In this paper, we formalize the translation of a small subset of Java bytecode into an imperative intermediate language similar to BoogiePL. We prove soundness of the translation by showing that each bytecode method whose BoogiePL translation can be veriﬁed, can also be veriﬁed in a logic that operates directly on bytecode.

Hermann Lehner, Peter Müller

Real-time Traffic