T. Arons, E. Elster, L. Fix, S. Mador-haim, M. Mishaeli et al., Formal Verification of Backward Compatibility of Microcode, CAV, pp.185-198, 2005.
DOI : 10.1007/11513988_20

S. Chaki, A. Gurfinkel, and O. Strichman, Regression verification for multithreaded programs, VMCAI, pp.119-135, 2012.

S. Ciobaca, D. Lucanu, V. Rusu, and G. Rosu, A language independent proof system for mutual program equivalence, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01030754

S. Craciunescu, Proving the Equivalence of CLP Programs, ICLP, LNCS 2401, pp.287-301, 2002.
DOI : 10.1007/3-540-45619-8_20

B. Godlin and O. Strichman, Regression verification, Proceedings of the 46th Annual Design Automation Conference on ZZZ, DAC '09
DOI : 10.1145/1629911.1630034

B. Godlin and O. Strichman, Inference rules for proving the equivalence of recursive procedures, Acta Informatica, vol.21, issue.7, pp.403-439, 2008.
DOI : 10.1007/s00236-008-0075-2

A. E. Haxthausen and F. Nickl, Pushouts of order-sorted algebraic specifications, AMAST, pp.132-147, 1996.
DOI : 10.1007/BFb0014312

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

S. Kundu, Z. Tatlock, and S. Lerner, Proving optimizations correct using parameterized program equivalence, PLDI, pp.327-337, 2009.
DOI : 10.1145/1543135.1542513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.348.3828

S. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo, SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs, CAV, pp.712-717, 2012.
DOI : 10.1007/978-3-642-31424-7_54

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

D. Lucanu and V. Rusu, Program equivalence by circular reasoning
DOI : 10.1007/978-3-642-38613-8_25
URL : https://hal.archives-ouvertes.fr/hal-01065830

D. Lucanu and V. Rusu, Program equivalence by circular reasoning, IFM, Lecture Notes in Computer Science, pp.362-377, 2013.
DOI : 10.1007/978-3-642-38613-8_25
URL : https://hal.archives-ouvertes.fr/hal-01065830

G. Necula, Translation validation for an optimizing compiler, PLDI, pp.83-94, 2000.

A. Pitts, Operational Semantics and Program Equivalence, Applied Semantics Summer School, pp.378-412, 2002.
DOI : 10.1007/3-540-45699-6_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.166

G. Ro¸suro¸su, C. Ellison, and W. Schulte, Matching logic: An alternative to Hoare/Floyd logic, AMAST, pp.142-162, 2010.

G. Ro¸suro¸su and A. Stefanescu, Checking reachability using matching logic, OOP- SLA, pp.555-574, 2012.