Patent ID: 8683441

Claim:
A computer-implemented method for equivalence checking of a first program and a second program, wherein the first and second programs are operative to receive a set of inputs, the method comprising: iteratively checking each valid pair of control paths for equivalence, wherein a valid pair of control paths is a pair of control paths for which there exists a representative value that causes the first and second programs to follow the pair of control paths, wherein the representative value comprising concrete values to the set of inputs; wherein said iteratively checking comprises: determining a representative value; determining a first control path in the first program associated with the representative value in the first program; determining a second control path in the second program associated with the representative value in the second program; and evaluating a symbolic comparison between output values determined in the first and the second control paths; and with respect to a valid pair comprising the first and second control paths, iteratively determining one or more additional valid pairs of control paths for which there exists a second representative value that is operable to cause one of the first or second program to follow the first or second control path respectfully and a counterpart control path to follow a different control path; wherein for each such second representative, evaluate a symbolic comparison between output values; wherein said iteratively determining control paths comprises: defining a symbolic formula, the symbolic formula comprising a disjunction between a first condition and a second condition, wherein the first condition is held for values for which the first control path is followed in the first program and the second control path is not followed in the second program, and wherein the second condition is held for values for which the first control path is not followed in the first program and the second control path is followed in the second program; determining a satisfying solution to the symbolic formula; and utilizing the satisfying solution to provide a representative value; whereby equivalence between the first program and the second program with respect to an equivalence class associated with the representative value is checked; whereby equivalence between the first and second programs is checked.