Patent ID: 8201116
Filing Date: 2012-06-12
Classification: G06F

Abstract:
1. A computer-implemented method for performing bounded model checking to a model in respect to a specification property, the method being performed by a computer including a processor and a memory, the method comprising: obtaining a UNSAT core of a first function from the memory, the first function being unsatisfiable if and only if the model holds the specification property within a first bound, wherein the UNSAT core is a portion of the first function that is unsatisfiable; calculating a second bound, the second bound is larger than the first bound; defining a second function based on the first function and based on the UNSAT core of the first function, the second function being unsatisfiable if and only if the model holds the specification property within the second bound; determining that the second function is unsatisfiable; calculating a third bound, the third bound is larger than the second bound based on the second function and based on the UNSAT core of the first function; and defining a third function, wherein the third function is unsatisfiable if and only if the model holds the specification property within the third bound, wherein the third function is defined based on the UNSAT core of the first function.