Software verification using model checking often translates programs into corresponding transition systems that model the program behavior. As software systems continue to grow in complexity and size, exhaustively checking a property on a transition graph becomes difficult. The focus of our research is the fundamental state explosion problem inherent in model checking that often prevents model checking from being applicable in real world design. Our research explores guided search, predicate abstration, disk based model checking, distributed model checking, etc. in an effort to extend model checking to larger systems. Much of our current work is in the Bogor framework, and we are also exploring new specification methods based on live sequence charts.