Hi Syshen,
I am not sure if it's answer to your question but the problem is undecidable although you can use SMT solver to verify both of your program. I don't have idea using SMT solver in OCaml ( right now I am learning it ) but I used it Haskell[1]. You can ask SMT solver to find a counter case for which your both programs are not producing the same output. If it gives you the such case then certainly your both code is not same. 


-Mukesh Tiwari
[1] http://hackage.haskell.org/package/sbv-2.10


On Sun, Sep 29, 2013 at 4:29 PM, 沈胜宇 <syshen@nudt.edu.cn> wrote:
Dear all:

I am working hard to optimize my ocaml program, but I am not sure whether the significantly modified version is equal to the old version.

So is there any research work on this topic?

Shen