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

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

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

S. Chaki, A. Gurfinkel, and O. Strichman, Regression Verification for Multi-threaded Programs, Lecture Notes in Computer Science, vol.6, issue.5, pp.119-135, 2012.
DOI : 10.1007/BF00268134

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

C. George and . Necula, Translation validation for an optimizing compiler, pp.83-94, 2000.

A. M. Pitts, Operational semantics and program equivalence Advanced Lectures, Applied Semantics, International Summer School, pp.378-412, 2000.
DOI : 10.1007/3-540-45699-6_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.166

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

S. Craciunescu, Proving the Equivalence of CLP Programs, International Conference of Logic Programming, pp.287-301, 2002.
DOI : 10.1007/3-540-45619-8_20

K. Shuvendu, C. Lahiri, M. Hawblitzel, H. Kawaguchi, and . Rebêlo, Symdiff: A language-agnostic semantic diff tool for imperative programs, Computer Aided Verification, pp.712-717, 2012.

F. Somenzi and A. Kuehlmann, Electronic Design Automation For Integrated Circuits Handbook, 2006.

G. Ro?u and D. Lucanu, Circular Coinduction: A Proof Theoretical Foundation, CALCO 2009, pp.127-144, 2009.
DOI : 10.1007/978-3-540-73859-6_25

G. Ro?u and T. ?erb?nu??, An overview of the K semantic framework, The Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010.
DOI : 10.1016/j.jlap.2010.03.012

G. Ro?u and A. Stefanescu, Checking reachability using matching logic, Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12, 2012.

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Approach to Symbolic Execution

M. Bonsangue, G. Caltais, E. Goriac, D. Lucanu, J. J. Rutten et al., A Decision Procedure for Bisimilarity of Generalized Regular Expressions, Proc. 13th Brazilian Symposium on Formal Methods, pp.226-241, 2011.
DOI : 10.1145/321312.321326