M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All about Maude ? a high-performance logical framework: how to specify, program and verify systems in Rewriting Logic, 2007.

G. Ro¸suro¸su and A. , Towards a unified theory of operational and axiomatic semantics, Proceedings of the 39th International Colloquium on Automata, Languages and Programming (ICALP'12), pp.2012-351

G. Ro¸suro¸su and A. , Checking reachability using matching logic, Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), pp.555-574, 2012.

G. Ro¸suro¸su, A. , S. ¸. Ciobâc?-a, and B. M. Moore, One-path reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013.

A. , S. ¸. Ciobâc?-a, R. Mereut¸?mereut¸?-a, B. M. Moore, T. F. et al., All-path reachability logic, Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA- TLCA'14), pp.425-440, 2014.

W. Swierstra, . Hoare, and . For-the-state-monad, A Hoare Logic for the State Monad, Theorem Proving in Higher Order Logics, 22nd International Conference. Proceedings, pp.440-451, 2009.
DOI : 10.1145/143165.143169

A. S. ¸tef?-anescu, D. Park, S. Yuwen, Y. Li, and G. Ro¸suro¸su, Semantics-based program verifiers for all languages, Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOP- SLA'16), 2016.

D. Lucanu, V. Rusu, and A. , Arusoaie, A Generic Framework for Symbolic Execution: a Coinductive Approach, Journal of Symbolic Computation
DOI : 10.1016/j.jsc.2016.07.012
URL : https://hal.inria.fr/hal-01238696/document

V. Rusu, D. Lucanu, T. Serbanuta, A. Arusoaie, A. Stefanescu et al., Language definitions as rewrite theories, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, pp.98-120, 2016.
DOI : 10.1016/j.jlamp.2015.09.001
URL : https://hal.archives-ouvertes.fr/hal-00950775

S. ¸tefan-ciobâc?-a, D. Lucanu, V. Rusu, and G. Rosu, A language-independent proof system for full program equivalence, Formal Asp, Comput, vol.28, issue.3, pp.469-497, 2016.

A. Arusoaie, D. Lucanu, and V. Rusu, Symbolic execution based on language transformation, Computer Languages, Systems & Structures, vol.44, pp.48-71, 2015.
DOI : 10.1016/j.cl.2015.08.004
URL : https://hal.archives-ouvertes.fr/hal-01186008

D. Lucanu and V. Rusu, Program equivalence by circular reasoning, Formal Asp, Comput, vol.27, issue.4, pp.701-726, 2015.
DOI : 10.1007/s00165-014-0319-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.372.5602

J. C. King, Symbolic execution and program testing, Communications of the ACM, vol.19, issue.7, pp.385-394, 1976.
DOI : 10.1145/360248.360252

C. S. and N. Rungta, Symbolic PathFinder: symbolic execution of Java bytecode, International Conference on Automated Software Engineering , ASE'10, pp.179-180, 2010.

P. Godefroid, N. Klarlund, and K. Sen, DART: directed automated random testing, Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp.213-223, 2005.

K. Sen, D. Marinov, and G. Agha, CUTE: a concolic unit testing engine for C, in: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp.263-272, 2005.

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler, EXE: automatically generating inputs of death, ACM Conference on Computer and Communications Security, pp.322-335, 2006.

J. De-halleux and N. Tillmann, Parameterized Unit Testing with Pex, Second International Conference, pp.171-181, 2008.
DOI : 10.1007/978-3-540-79124-9_12

C. Cadar, D. Dunbar, and D. Engler, Klee: unassisted and automatic generation of high-coverage tests for complex systems programs, Proc. 8th USENIX conference on Operating systems design and implementation, OSDI'08, pp.209-224, 2008.

A. Coen-porisini, G. Denaro, C. Ghezzi, and M. Pezzé, Using symbolic execution for verifying safety-critical systems, ACM SIGSOFT Software Engineering Notes, vol.26, issue.5, pp.142-151, 2001.
DOI : 10.1145/503271.503230
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.9662

J. Jaffar, V. Murali, J. A. Navas, and A. E. Santosa, TRACER: A Symbolic Execution Tool for Verification, Computer Aided Verification -24th International Conference Proceedings, pp.758-766, 2012.
DOI : 10.1007/978-3-642-31424-7_61
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.2475

D. A. Ramos and D. R. Engler, Practical, Low-Effort Equivalence Verification of Real Code, Proceedings of the 23rd international conference on Computer aided verification, pp.669-685, 2011.
DOI : 10.1109/FMCAD.2008.ECP.10

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

G. C. Necula, Translation validation for an optimizing compiler, PLDI, ACM, pp.83-94, 2000.
DOI : 10.1145/349299.349314
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2567

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, CAV, pp.185-198, 2005.
DOI : 10.1007/11513988_20

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

O. Strichman, Regression Verification: Proving the Equivalence of Similar Programs, CAV, p.63, 2009.
DOI : 10.1007/978-3-642-02658-4_8

B. Godlin and O. Strichman, Inference Rules for Proving the Equivalence of Recursive Procedures, Essays in Memory of Amir Pnueli, pp.167-184, 2010.
DOI : 10.1007/BFb0055057

K. Bae, S. Escobar, and J. Meseguer, Abstract logical model checking of infinitestate systems using narrowing, 24th International Conference on Rewriting Techniques and Applications, RTA 2013 of LIPIcs, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.81-96, 2013.

C. Rocha, J. Meseguer, and C. A. Muñoz, Rewriting modulo SMT and open system analysis, in: Rewriting Logic and Its Applications -10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, pp.247-262, 2014.

C. Rocha, J. Meseguer, and C. Muñoz, Rewriting modulo {SMT} and open system analysis, Journal of Logical and Algebraic Methods in Programming, 2016.
DOI : 10.1016/j.jlamp.2016.10.001
URL : http://hdl.handle.net/2060/20150014338

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

V. Rusu and A. Arusoaie, Proving Reachability-Logic Formulas Incrementally, Revised Selected Papers Lecture Notes in Computer Science, vol.10, issue.2, pp.134-151, 2016.
DOI : 10.1007/978-3-642-37036-6_8
URL : https://hal.archives-ouvertes.fr/hal-01282379

G. Ro¸suro¸su, C. Ellison, and W. Schulte, Matching Logic: An Alternative to Hoare/Floyd Logic, Proceedings of the 13th International Conference on Algebraic Methodology And Software Technology (AMAST '10), pp.142-162, 2010.
DOI : 10.1145/514188.514190

G. Ro¸suro¸su and A. , Matching Logic: A New Program Verification Approach (NIER Track, ICSE'11: Proceedings of the 30th International Conference on Software Engineering, pp.868-871, 2011.

G. Ro¸suro¸su, Matching logic ? extended abstract, Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA'15) of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.5-21, 2015.

S. Freevars, we also have (?, µ ) |= ? l ?? l . Thus, using the unquantified version of ?, i.e., ? ? l ?? l ? ? r ?? r , we obtain ? ? ? ? . We can now apply Lemma 8 and obtain a pattern ? ? ? with FreeVars(? ? ? ) ? V ar b such that ??? ? s ? ? ?? and (? , ? ) |= ? ?? , for some valuation ? such that ? | FreeVars(???) = ?| FreeVars(???)

. Specifically, ? ? ? ? (? l ? ? r ), with ? ? ? Id| Var \FreeVars(? l ) and ? : FreeVars(? l ) ? T ? (FreeVars(?)) ? match? = (?, ? l ) Let ? (?X, Y )(? (? r ) ? ? ? ? (? l ? ? r ) By Def

F. We, FreeVars(?) ? (FreeVars(? r ) \ FreeVars

. Freevars, But (FreeVars(?) \ X) ? FreeVars(?) and by Assumption 1, FreeVars(? r ) \ Y ) \ FreeVars(? l ) = ?. Hence, FreeVars(? (? r )) ? FreeVars(?)

F. Next, ? FreeVars(? (? l )) using Assumption 1, and we obtain FreeVars(? (? l )) ? FreeVars(?), and then FreeVars

. Finally, Assumption 1 we have FreeVars(? r ) ? FreeVars(? l ) ? Y , thus, FreeVars(? (? r )) ? FreeVars(?)?Y, We then obtain FreeVars(? (? r ))\(X ?Y ) ?

. Proof, Let ? (?X)??? and ? ? l ?? l ? (?Y )? r ?? r . Thus we have ? = (?X, Y )? (? r )?(? ? ? (? r ) ? ? (? l )) for some substitution ? : FreeVars(? l ) ?