A method for Formal Verification that involves checking certain properties o exhaustive search of all possible states the program could enter during execution.