using a computer processor coupled to memory to execute the step of:

inputting a program containing elements written in a plurality of languages;

inputting a rule set specifying allowable behaviors of a correct program;

transforming the input program, wherein said transforming comprises preserving sufficient data and control flow information relating to the input program in a predetermined amount and to a predetermined degree of precision; and

wherein the transforming includes translating the program to a target language as an output program;

detecting in the input program any violation relating to the rule set, wherein said detecting comprises employing the target language in detecting a violation relating to the rule set;

ensuring that the input program avoids any violation relating to the rule set;

mapping back to an original source code any violation relating to the rule set;

wherein at least a portion of the input program is written in C programming language, and the portion is translated into Java programming language, and further wherein the translating step comprises:

implementing function pointers using virtual method and anonymous inner classes in the output program, said pointers being mapped to arrays of length one in Java programming language, said implementing function pointers comprises:

mapping each function pointer type to an Fn class, the Fn class being constructed with a virtual method named idrCall overloaded multiple times, wherein for each signature of different length used at an indirect call site anywhere in the software program idrCall is overloaded one more time;

extending an Fn class anonymously whenever an address of a function is being taken;

overriding a virtual member method with matching arguments to now branch to a destination function, and

relinking indirect call sites to transit via a virtual function; and

implementing goto translation in a way that does not modify control and data flow of the input program;

wherein Basic types in C programming language are mapped directly to the same types in Java programming language, Structures and unions are mapped to classes with the corresponding fields set to public, and Functions become public methods of a global class representing an entire file being translated; and

employing the target language to verify that said rules are not violated.