Author:
Mana Taghdiri, Franjo Ivancic
Place:
NEC Laboratories America, Inc. Technical report TR-2004-L070, 2004
Date: Sep. 2004
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.

BibTex

@TechReport{taghdiri-tr-2004,

    author      = "M. Taghdiri and F. Ivancic",

    title       = {Analyzing Java Programs with F-Soft},

    institution = {NEC Laboratories America, Inc},

    number      = {TR-2004-L070},

    address     = {Princeton, NJ},

    year        = {2004}