Home | Legals | Data Protection | Sitemap | KIT

Analyzing Java Programs with F-Soft

Analyzing Java Programs with F-Soft

Mana Taghdiri, Franjo Ivancic


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 differs from the standard existing methods. Using this Java frontend, F-Soft is now unique amongst verification 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.


    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}