Transition System Generation Papers

The Bandera tools are designed to compile a Java program to a finite-state model that can be processed by multiple model-checking systems. This is accomplished by first translating the Java program to a model specified in a guarded command language called BIR (Bandera Intermediate Representation). The BIR model can then translated into the input languages of several different model-checking tools. Currently, there are translations from BIR to Promela (the input language of SPIN) and the SMV input language. There is ongoing work on a BIR to SAL translator (SAL is an intermediate language for verification tools developed at Stanford and SRI).

The BIR module can also be used in a stand-alone configuration (with out going through the slicing or ABPS components). It provides a convenient way to get a model for multiple model-checking tools.

  • Using Shape Analysis to Reduce Finite-State Models of Concurrent Java Programs. James C. Corbett. ICS-TR-98-20
  • Constructing Compact Models of Concurrent Java Programs, James C. Corbett, In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), March, 1998.
  • Translating Ada Programs for Model Checking : A Tutorial, Matthew B. Dwyer, James C. Corbett and Corina S. Pasareanu. This paper is published as KSU CIS TR 98-12. An online version of this paper (with additional resources linked) is available here.
  • BIR Documentation