From CIL to Java bytecode: Semantics-based translation for static analysis leveraging

A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall process of translation and analysis is fast, scales to industrial programs, and introduces a negligible number of false alarms. The main contribution of this work is to leverage existing, mature, and sound analyzers for Java bytecode by applying them also to the wide range of .Net software systems. Experimental results show the actual effectiveness of this approach when applied to all the system libraries of the Microsoft .Net framework version 4.0.30319 (about 5 MLOCs).