The Bandera back end is like a code generator, taking the sliced and abstracted program and producing verifier-specific representations for targetted verifiers. The back end components communicate through BIR, the Bandera Intermediate Representation, an intermediary between compiler-based representations and verifier-based representations. As shown in Figure 1, the back end has one fixed component called BIRC (Bandera Intermediate Representation Constructor) that accepts a restricted form of Jimple and produces BIR. For each supported verifier, there is also a translator component that accepts the program represented in BIR and generates input for that verifier. Currently, translators for SPIN, dSPIN, and SMV are complete, and translators for FDR2, XMC, and Stanford's forthcoming SAL model checker are under construction.
BIR is a guarded command language for describing state transition systems. The main purpose of BIR is to provide a simple interface for writing translators for target verifiers--to use Bandera with a new verifier, one must only write a translator from BIR to the input language of the verifier. The guarded command style of BIR meshes well with the input languages of existing model checkers.
BIR contains some higher-level constructs to facilitate modeling Java, such as threads, Java-like locks (supporting wait/notify), and a bounded form of heap allocation. Rather than choose an implementation of these constructs and remove them from BIR (e.g., model a lock as a boolean variable), we allow the translators to implement these constructs in whatever way is most efficient in the verifier input language. BIR also provides other kinds of information that can aid translators in producing more compact models. For example, a guarded command can be labeled invisible, indicating that it can be executed atomically with its successor. The set of local variables that are live at each control location can be specified (dead variables can be set to a fixed value for SPIN or left unconstrained for SMV).