Requirements

Machine requirements:

1. Minimum Processor: Intel Pentium III 600 MHz or equivalent.
2. Memory: 128 MB (minimum), 256 MB or more is recommended.
3. Hard drive free space: 60 MB (minimum). May need some space in user's home directory for logging and custom files, typically less than 1 MB.

Supported operating systems:

• Windows 95/98/Me
• Windows 2000
• Windows 4.0
• Sun OS 5.6 or 5.7
• Linux with kernel 2.2.14 or better.

We are aware that Java programs can be run on any platform with Java compiler. Although we endeavor to make Bandera run in all Java-supporting platforms, we have not yet tested it in platforms other than those mentioned above.

We currently use Sun's standard JDK version 1.3 for Bandera development. We are aware that there are many Java compilers. Even if it claims compatibility with the standard JDK, we are not certain that Bandera would compile or run. Earlier versions of standard JDK are also not recommended.

Bandera supports JPF, Spin, dSpin, and NuSMV for this release. However none of these checkers are bundled with the distribution -- you need to separately install those model checkers if you intend to use Bandera with them.

For Spin, we expect that the main model checker filename is spin. For SMV, it should be NuSMV. For DSpin, it should be dspin. Please make sure that all of these are installed in the directories mentioned in the path. To use JPF with Bandera, simply put it with all its supporting packages into the same directory with Bandera.

Make sure that you have your C compiler and C preprocessor properly installed and their directory is mentioned in the path. This is necessary because the Spin model checker produces C files that have to be preprocessed and compiled. We assume the C compiler is GNU's gcc and that the C preprocessor is GNU's cpp. The gcc and cpp versions are not specific, but our testing shows that version 2.91 or above is fine. For Windows environment, DJGPP's gcc is just working fine.