G. Ro?u and A. ?tef?nescu, Towards a Unified Theory of Operational and Axiomatic Semantics, Proceedings of the 39th International Colloquium on Automata, Languages and Programming, pp.351-363, 2012.
DOI : 10.1007/978-3-642-31585-5_33

G. Ro?u and A. ?tef?nescu, 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?u, A. ?tef?nescu, ?. Ciobâc?, and B. M. Moore, Onepath reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013.

A. ?tef?nescu, ?. Ciobâc?, R. Mereu??, B. M. Moore, G. Traian-florin-?erb?nu?? 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.
DOI : 10.1007/978-3-319-08918-8_29

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Framework for Symbolic Execution, 2015.
DOI : 10.1007/978-3-319-02654-1_16
URL : https://hal.archives-ouvertes.fr/hal-00853588

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Framework for Symbolic Execution Available at https, 2015.

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.

L. De, M. , and N. Bjørner, Z3: An efficient SMT solver In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS'08, pp.337-340, 2008.

G. Ro?u, 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?u and A. ?tef?nescu, Matching logic, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.868-871, 2011.
DOI : 10.1145/1985793.1985928

G. Ro?u, Matching logic ? extended abstract, Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA'15), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pp.5-21, 2015.

D. Lucanu, V. Rusu, A. Arusoaie, and D. Nowak, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Logic, Rewriting, and Concurrency -Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, pp.451-474, 2015.
DOI : 10.1007/978-3-319-23165-5_21
URL : https://hal.archives-ouvertes.fr/hal-01158941

W. Visser, K. Havelund, and G. P. Brat, Seungjoon Park, and Flavio Lerda. Model checking programs, Automated Software Engineering, vol.10, issue.2, pp.203-232, 2003.
DOI : 10.1023/A:1022920129859

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

P. Willem, F. S. De-roever, U. De-boer, J. Hannemann, and . Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Cambridge Tracts in Theoretical Computer Science, 2001.

V. Rusu, D. Lucanu, . Traian-florin, A. Serbanuta, A. Arusoaie 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. Proof, ?Y )? ?? we consider an arbitrary pair (?, ?) such that (?, ?) |= ? and an arbitrary complete path ? Since (?Y )? captures all terminal configurations for ???, there exists ? with ? | Var \Y = ?| Var \Y such that ? = ? (? ) But since (?Y )? is invariant at (?Y )? starting from ???, we obtain ? |= ? . Thus, for an arbitrary pair (?, ?) such that (?, ?) |= ? and an arbitrary complete path ? ? S · · · ? S ? , we have obtained ? with ? | Var \Y = ?| Var \Y such that (? , ? ) |= ? ?? , which is S |= ??? ? (?Y )? ?? according to Definition 13. (?) We have to show that S |= ??? ? (?Y )? ?? implies (i) (?Y )? is invariant at (?Y )? starting from ??? and (ii) (?Y )? captures all terminal configurations for ???. We first prove (i), ) |= ???, ? | Var \Y = ?| Var \Y , and ? n = ? (? )

?. S-·-·-·-?-s-?-n-is-complete, From S |= ??? ? (?Y )? ?? we obtain that there exists 0 ? i ? n and a valuation ? with ? | Var \Y = ?| Var \Y such that (? i , ? ) |= ? ?? . Thus, ? i = ? (? ) is terminal as well, and thus ? i = ? n , since there cannot be two terminal configurations on one path. Thus, ? n = ? (? ) and ? |= ? . We now show ? |= ?, FreeVars(? ) ? FreeVars(?)?FreeVars(? ). Consider then any variable x ? FreeVars(? )

?. Freevars, By Remark 1, from ? (? ) = ? (? )(= ? n ) we obtain ? | FreeVars(? ) = ? | FreeVars(? ) and thus ? (x) = ? (x)

. Thus and ?. S. Freevars, ? such that (? 0 , ?) |= ???, ? | Var \Y = ?| Var \Y , and ? n = ? (? ), ? |= ? holds This is just (?Y )? is invariant at (?Y )? starting from ???, which proves (i) There remains to prove (ii) Consider now an arbitrary terminal path ? 0 ? S · · · ? S ? n and a valuation ? such that (? 0 , ?) |= ???, Since S |= ??? ? (?Y )? ?? we obtain (? n , ?) |= (?Y )? ?? . In particular, (? n , ?) |= (?Y )? , i.e., (?Y )? captures all terminal configurations for ???, which proves (ii), the (?) implication, and the proposition

. Lemma-8, Consider a terminal rl formula ??? ? (?Y )? ?? . If the procedure in Figure 2 terminates with Failure = false, then (?Y )? is an invariant at (?Y )? starting from ???

?. Freevars, ? )\FreeVars(???) = ? | FreeVars(? )\FreeVars(???

?. Freevars, ???) = ? | FreeVars(???) = ? | FreeVars(???) , and ? | FreeVars(?n)\FreeVars(???) = ? | FreeVars(?n)\FreeVars(???)