D. Lucanu and V. Rusu, Program Equivalence by Circular Reasoning, In Integrated Formal Methods Lecture Notes in Computer Science, vol.7940, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01065830

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Framework for Symbolic Execution, 6th International Conference on Software Language Engineering, pp.281-301, 2013.
DOI : 10.1007/978-3-319-02654-1_16

URL : https://hal.archives-ouvertes.fr/hal-00853588

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

S. Escobar and J. Meseguer, Symbolic Model Checking of Infinite-State Systems Using Narrowing, Term Rewriting and Applications, 18th International Conference, pp.153-168, 2007.
DOI : 10.1007/978-3-540-73449-9_13

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

L. Simon, A. Bansal, A. Mallya, and G. Gupta, Co-Logic Programming: Extending Logic Programming with Coinduction, ICALP, pp.472-483, 2007.
DOI : 10.1007/978-3-540-73420-8_42

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.9618

D. Ancona and E. Zucca, Corecursive Featherweight Java, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP '12, pp.3-10
DOI : 10.1145/2318202.2318205

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.413.5137

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

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.

L. De, M. , and N. Bjørner, Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems RESEARCH CENTRE LILLE ? NORD EUROPE Parc scientifique de la Haute-Borne 40 avenue Halley -Bât A -Park Plaza 59650 Villeneuve d'Ascq, pp.337-340, 2008.