The impact of verification technologies would be much greater if they could not only verify existing information systems, but also synthesize or discover new ones. In our previous study, we tried to discover new algorithms that satisfy a given specification, by first defining a space of algorithms, and then checking each algorithm in the space against the specification, using an automatic verifier, i.e., model checker. Needless to say, the most serious problem of this approach is in search space explosion. In this paper, we describe case studies in which we employed symbolic model checking using BDD and searched for synchronization algorithms. By employing symbolic model checking, we could speed up enumeration and verification of algorithms. We also discuss the use of approximation for reducing the search space.