For the state/event linear temporal logic SE-LTL, an SAT-based Bounded Model Checking procedure which avoids the space blow up of BDDs is presented. For SE-LTL-_X, it is shown how to integrate the procedure and the stuttering equivalent technique. The integration speeds up the verification procedure. Furthermore, a framework for model checking concurrent software systems which integrates three powerful verification techniques is presented: SAT-based Bounded Model Checking, counterexample-guided abstraction refinement and compositional reasoning. In the framework the abstraction and refinement steps are performed over each component separately, and the model checking step is symbolic. Example shows that the framework can reduce verification time and space.