Conditional Model Checking
Source: University of Passau
Software model checking, as an undecidable problem, has three possible outcomes: the program satisfies the specification, the program does not satisfy the specification, and the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. The authors give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition.