What about infinite state?
	• Model checking does not apply to infinite state specifications – The iterative algorithm will not reach a fixpoint • Theorem proving applies well to infinite state specifications, but has generally proved to be unsatisfactory in practice • One approach is to abstract infinite state specifications into finite state ones – Doing this while preserving properties is hard • D. Jackson et al.’s Nitpick approach – Find counterexamples (errors), but don’t “prove” anything