Automatically exploring every reachable state of a system model to verify that it satisfies stated properties.