1. 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; evaluating a symbolic comparison between output values determined in the first and the second control paths; and whereby equivalence between the first program and the second program with respect to an equivalence class associated with the representative value is checked.