Patent ID: 8271253

Claim:
A method for performing invariant checking of a system, the method comprising: generating, by a computational device, an abstract control model of the system from a concrete model of the system based on control paths and predicates, the abstract control model of the system including control flow information regarding the system, wherein the concrete model is an original representation of the system, and wherein the abstract control model allows for a simulation of the system to prove or disprove one more selected invariants; determining, whether a selected invariant includes only control variables of the system; in response to determining that the selected invariant includes only the control variables of the system, performing a depth-first search of the abstract control model to determine satisfiablity of the selected invariant; and in response to determining that the selected invariant does not include only the control variable of the system, performing: generating, by the computational device, execution traces of the system using the control flow information of the abstract control model; providing, by the computational device, the execution traces for use as constraints on the concrete model during a depth-first search of the concrete model to determine whether the selected invariant of the system is satisfiable, wherein the execution traces are based on a likelihood of an execution trace to lead to a disproving of the selected invariant based on a cone of influence of variables referred to in the selected invariant; a variable is within the cone of influence of another variable if the variable depends on the other variable; and in a control flow graph corresponding to the concrete model of the system those control flow graph paths that include a defined variable within the cone of influence of a variable referred to in the selected invariant are more likely to lead to a contradiction of the selected invariant in comparison to those control flow graph paths that do not include the defined variable within the cone of influence of the variable referred to in the selected invariant.