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.