Current version: BSP 1.0 BSP is an interpreter for Boolean Symbolic Programs, i.e. programs manipulating boolean functions.

BSP can be used as a symbolic model checker simply by writing in BSP your favorite symbolic model checking algorithm.

Essentially BSP is a logic based interface to an OBDD package. Writing symbolic algorithms with BSP is easier than using C primitives for OBBD manipulations. With little effort you can experiment with your brand new symbolic algorithm. Once you think the effort is worth you can turn to C primitives for OBBD manipulations.

So far BSP works on SOLARIS (SUN) and on Linux machines.

You can download BSP from here.


Browse all versions
BSP 1.0 latest version bsp.1.0.tgz 845 KB