Home | Impressum | 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

Datum: 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.