Patent ID: 8271253
Filing Date: 2012-09-18
Classification: G06F

Abstract:
1. 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