Bandera is built on top of the Soot Java compiler framework developed by Laurie Hendren's Sable group at the University of McGill [15]. In the Soot framework, Java programs are translated to an intermediate language called Jimple. Jimple was originally developed to be the target language of a Java decompiler (i.e., the Soot tools provide a component for decompiling Java class files (byte code) to Jimple). Thus, Jimple is essentially a language of control-flow graphs where (a) statements appear in three-address-code form (the explicit stack manipulation inherent in JVM instructions has been removed by introducing temporary variables), and (b) various Java constructs such as method invocations and synchronized statements are represented in terms of their virtual machine counterparts (such as invokevirtual, and monitorenter, monitorexit).