Model Checking Laboratory

BSP

Details

Category: Software

Last Updated on Sunday, 02 December 2012 15:33

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.