This paper presents a novel technique for abstracting designs in order to increase the efficiency of formal property checking. Bounded Model Checking (BMC), using Satisfiability (SAT) techniques, are beginning to be widely used for checking properties of designs. Recent approaches using sequential ATPG techniques, which harness the structural information of the design, have been shown to perform better than SAT-based BMC. However, these techniques require an effective methodology to deal with the size of commercial designs. A program slicing methodology that has been shown to accelerate sequential ATPG is adapted and integrated into an ATPG-based BMC framework. Furthermore, a generalization of the ATPG-based approach, which checks for unbounded liveness, is also presented.