An algebraic method for verification of arithmetic program

This paper proposes an algebraic method to prove the correctness of Arithmetic Program which halts in finitely number of steps. The main routine is to simulate the program by a BSS computational model over the real numbers, thus it can be represented by a system of polynomial equations. The problem of proving program correctness will be translated into an algebraic one, which decides if the zeros of two systems of polynomial equations equals. The proof complexity of this method depends on the computational steps of a program.Computer Science, Theory & MethodsCPCI-S(ISTP)