List of Projects Dealing with Verification of Functional Equivalence of Programs

Some of these may not deal directly with functional equivalence, but could be applicable to that problem.

 * [https://vsl.cis.udel.edu/tass Toolkit for Accurate Scientific Software] (TASS)
 * [https://vsl.cis.udel.edu/mpi-spin/index.html MPI-Spin]
 * [http://klee.llvm.org KLEE]
   * [http://blog.gmane.org/gmane.comp.compilers.llvm.klee Discussion]
   * [http://keeda.stanford.edu/~daramos/ucklee-cav-2011.pdf UC-KLEE]
   * [http://www.pcc.me.uk/~peter/klee-fp KLEE-FP] and  [http://www.doc.ic.ac.uk/~pcc03/eurosys11klee.pdf paper]
 * [http://www.cprover.org/cbmc CBMC]
 * [http://www.cprover.org/satabs SATABS]
 * [http://www.cprover.org/wolverine Wolverine]
 * [http://cseweb.ucsd.edu/~mstepp/peggy Peggy]
 * [http://research.microsoft.com/en-us/projects/symdiff SymDiff]
 * [http://www.synopsys.com/Tools/Verification/FormalEquivalence/Pages/Formality.aspx Synopsys Formality]
 * [http://pincette-project.haifa.il.ibm.com Pincette]
 * [http://ie.technion.ac.il/~ofers/TVS.htm TVS]
 * RVT: [http://ie.technion.ac.il/~ofers/publications/rvt_tech.pdf Paper]
 * ISA [http://www.springerlink.com/content/k7244m230266g8r2/ paper] and  [http://www.kotnet.org/~skimo/loop/isa-0.08.tar.bz2 tool]