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
>