1. A method of verifying a software program comprising: modeling the software program, which can have bounded recursion, as a Boolean representation comprising a plurality of basic blocks, each basic block representing a sequence of one or more instructions in the software program as a set of parallel assignments and a set of transitions to other basic blocks; and applying a SAT-based model checker to the Boolean representation of the software program.