Based on an initial prototype from the Soot group, the Bandera group has developed it's own Java front-end called JJJC (Java-to-Jimple-to-Java Compiler) that translates from Java to Jimple. JJJC also maintains data structures that are used by a Jimple-Java Mapper to move back and forth between Java and Jimple. For instance, JJJC can also decompile Jimple that has been transformed by Bandera's slicing and abstraction components back to Java. Thus, the Bandera slicer and abstraction tools can be viewed as source-to-source transformations. This is useful if one desires to use other verification tools that work at the Java source level in conjunction with Bandera. The Jimple-Java Mapper is also invoked during the process of mapping a model-checker counterexample back to the Java source level.