A method for symbolic model checking for sequential systems using a combination of state-based and state-less approaches. A state-based method is used to compute frontier states by building transition relations on-the-fly using control flow information of the system, and performing successive image computations until a memory bound is reached, and efficiently storing only the new frontier states as disjunctive partitions of Boolean and Arithmetic expressions. A stateless method is used to check reachability of given goal states from a heuristically chosen set of frontier states until depth/time bound is reached. These two methods are alternated until one of the following occurs: all frontier states are explored, all goal states are reached, all computing resources are exhausted. Even though we do not store the entire reachable state set, we guarantee a complete coverage for terminating programs without the need to compute a fixed-point.