| 摘要 |
This source code equivalence verification device is provided with: a symbolic execution calculation unit which performs symbolic execution on both an original source code and a modified version of the original source code; an equivalence verification expression generation unit which generates, using the results of the symbolic execution performed by the symbolic execution calculation unit, equivalence verification expressions for verifying equivalence between the original source code and the modified source code; an equivalence verification expression verification unit which verifies the equivalence verification expressions generated by the equivalence verification expression generation unit; a correction candidate generation unit which generates a correction candidate, on the basis of which the modified source code is to be corrected so as to be equivalent to the original source code, if the results of the verification of the equivalence verification expressions by the equivalence verification expression verification unit indicate that the modified source code is not equivalent to the original source code; and a verification result generation unit which generates a verification result report using the results of the verification performed by the equivalence verification expression verification unit and the correction candidate generated by the correction candidate generation unit. |
