Bebop: A symbolic model checker for boolean programs

Abstract. We present the design, implementation and empirical evalu-ation of Bebop|a symbolic model checker for boolean programs. Bebop represents control ow explicitly, and sets of states implicitly using BDDs. By harnessing the inherent modularity in procedural abstraction and ex-ploiting the locality of variable scoping, Bebop is able to model check boolean programs with several thousand lines of code, hundreds of pro-cedures, and several thousand variables in a few minutes.