BSP, an interpreter for Boolean Symbolic Programs
BSP can be used as a symbolic model checker simply by writing in BSP your favorite symbolic model checking algorithm.
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.