Specialization with constrained generalization for software model checking