An alternative: model checking
	• Evaluate temporal properties of finite state systems – Guarantee a property is true or return a counterexample – Ex: Is it true that we can never enter an error state? – Ex: Are we able to handle a reset from any state? • Extremely successfully for hardware verification – Intel got into the game after the FDIV error • Open question: applicable to software specifications?