This paper presents an extension to the F-Soft frontend parser that allows us to analyze Java programs as well as C programs. A Java to C translator is developed and presented here for the purpose of checking Java programs with respect to a given property using F-Soft. The translation is done via Jimple, an intermediate language with 3-address instructions. The goal is to generate a C program that is straightforward to analyze using F-Soft. Therefore, in some cases, our translation technique diﬀers from the standard existing methods. Using this Java frontend, F-Soft is now unique amongst veriﬁcation tools in that it is capable of analyzing both Java and C programs. Furthermore, it is one of the few tools that can handle Java checked exceptions and dynamic dispatch.
Analyzing Java Programs with F-Soft
Mana Taghdiri, Franjo Ivancic
NEC Laboratories America, Inc. Technical report TR-2004-L070, 2004