W. Ahrendt, The KeY tool. Software and Systems Modeling, pp.32-54, 2005.

A. Armando, M. Benerecetti, and J. Mantovani, Model Checking Linear Programs with Arrays, Electronic Notes in Theoretical Computer Science, vol.144, issue.3, pp.79-94, 2006.
DOI : 10.1016/j.entcs.2006.01.006

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

A. Arusoaie, D. Lucanu, and V. Rusu, Symbolic execution based on language transformation Computer Languages, Systems & Structures, 2015. To appear, preprint available at https

M. Barnett, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, Proc. 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS'04, pp.49-69, 2005.
DOI : 10.1007/978-3-540-30569-9_3

J. Berdine, C. Calcagno, and P. W. Hearn, Symbolic Execution with Separation Logic, Yi [48], pp.52-68
DOI : 10.1007/11575467_5

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.

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.

E. Clarke and D. Kroening, Hardware verification using ANSI-C programs as a reference, Proceedings of the 2003 Asia and South Pacific Design Automation Conference, ASP-DAC '03, pp.308-311, 2003.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. M. Oliet et al., All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, 2007.

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

H. Thomas, C. Cormen, R. L. Stein, C. E. Rivest, and . Leiserson, Introduction to Algorithms, 2001.

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

H. Cui, G. Hu, J. Wu, and J. Yang, Verifying systems rules using rule-directed symbolic execution, ACM SIGPLAN Notices, vol.48, issue.4, pp.329-342, 2013.
DOI : 10.1145/2499368.2451152
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.310.2374

J. De, H. , and N. Tillmann, Parameterized unit testing with Pex, TAP, pp.171-181, 2008.

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.

S. Escobar, J. Meseguer, and R. Sasse, Variant Narrowing and Equational Unification, Electronic Notes in Theoretical Computer Science, vol.238, issue.3, pp.103-119, 2009.
DOI : 10.1016/j.entcs.2009.05.015

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. Godefroid, N. Klarlund, and K. Sen, DART: directed automated random testing, PLDI, pp.213-223, 2005.

D. Harel, D. Kozen, and J. Tiuryn, Dynamic logic, Handbook of Philosophical Logic, pp.497-604, 1984.

B. Jacobs, J. Smans, and F. Piessens, A Quick Tour of the VeriFast Program Verifier, Proceedings of the 8th Asian conference on Programming languages and systems, APLAS'10, pp.304-311, 2010.
DOI : 10.1007/978-3-642-17164-2_21

J. Jaffar, V. Murali, J. A. Navas, and A. E. Santosa, TRACER: A Symbolic Execution Tool for Verification, Proc. 24th international conference on Computer Aided Verification, CAV'12, pp.758-766, 2012.
DOI : 10.1007/978-3-642-31424-7_61

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

E. Donald, J. H. Knuth, V. R. Morris, and . Pratt, Fast pattern matching in strings, SIAM Journal of Computing, vol.6, issue.2, pp.323-350, 1977.

D. Lucanu, V. Rusu, A. Arusoaie, and D. Nowak, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Logic, Rewriting, and Concurrency -Festschrift Symposium in Honor of José Meseguer, 2015.
DOI : 10.1007/978-3-319-23165-5_21
URL : https://hal.archives-ouvertes.fr/hal-01158941

D. Lucanu and T. ?erb?nu??, CinK -an exercise on how to think in K, 2013.

J. Meseguer and P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, pp.123-160, 2007.

B. Moore and G. Ro?u, Program verification by coinduction, 2015.

C. S. P?s?reanu and W. Visser, Verification of Java Programs Using Symbolic Execution and Invariant Generation, LNCS, vol.2989, pp.164-181, 2004.
DOI : 10.1007/978-3-540-24732-6_13

C. S. P?s?reanu and W. Visser, A survey of new trends in symbolic execution for software testing and analysis, International Journal on Software Tools for Technology Transfer, vol.17, issue.2, pp.339-353, 2009.
DOI : 10.1007/s10009-009-0118-1

A. David, D. R. Ramos, and . Engler, Practical, low-effort equivalence verification of real code, Proceedings of the 23rd international conference on Computer aided verification, pp.669-685, 2011.

C. John and . Reynolds, Separation logic: A logic for shared mutable data structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02, pp.55-74, 2002.

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.

G. Ro?u and A. ?tef?nescu, From Hoare Logic to Matching Logic Reachability, Proceedings of the 18th International Symposium on Formal Methods (FM'12), pp.387-402, 2012.
DOI : 10.1007/978-3-642-32759-9_32

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

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-traian-florin and . ?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. ?tef?nescu, Checking reachability using matching logic Also available as technical report http, OOPSLA, pp.555-574, 2012.

V. Rusu, D. Lucanu, A. Traian-florin-?erb?nu??, A. Arusoaie, G. ?tef?nescu et al., Language definitions as rewrite theories, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, p.48, 2015.
DOI : 10.1016/j.jlamp.2015.09.001
URL : https://hal.archives-ouvertes.fr/hal-00950775

D. Sangiorgi, An Introduction to Bisimulation and Coinduction A preliminary version of Chapter, 2012.

H. Peter, B. Schmitt, and . Weiß, Inferring invariants by symbolic execution, CEUR Workshop Proceedings. CEUR-WS.org, 2007.

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

G. Traian-florin-?erb?nu??, J. Ro?u, and . Meseguer, A rewriting logic approach to operational semantics, Information and Computation, vol.207, issue.2, pp.305-340, 2009.
DOI : 10.1016/j.ic.2008.03.026

@. We-prove-? and =. ??, ? = ? 1 (??) = (? 1 ?)? and since ? ? µ(? 1 , ?), ? 1 ? ? =A ?. Hence, (? 1 ?)? ? =A ??, and since ? =A is the equality "=" in T , we have (? 1 ?)? = ??. Using the hypothesis var (?) ? var (? 1 , ? 2 ) = ? we obtain var (?) ? var (? 1 ) = ?, and since ? is the identity everywhere except perhaps on var (? 1 ) and ? ?? we obtain that ? and ? coincide on var (?); hence

@. We, from hypothesis (? , ?) |= ? 2 ? ? ? 1 ? ? ? 2 ? ? ? we obtain in particular ? |= ?. Using again the hypothesis var (?) ? var (? 1 , ? 2 ) = ? we obtain that that ? and ? coincide on var (?), hence, ? |= ? as well

. Finally, we prove (?): (? , ?) |= ? 2 ? 2 ? ? 2 . We prove ? |= ? 2 by analogy with ? |= ? 1

W. Recapitulating and . Have, From (?) and (?) we get ? ? {?1 ? ? ? ?2} ? . Using that and (?) and Lemma 4.1, which says that symbolic execution steps forward-simulate concrete ones, we obtain that there exists ? such that ? ? s ?1 ? ? ? ?2} ? and (? , ?) |= ? . By definition of ? s , ? ? {?1 ? ? ? ?2} (?), which proves (? , ?) |= ? {?1 ? ? ? ?2} (?), i.e., ? ? ? {?1 ? ? ? ?2} (?) and the conclusion of the (?) inclusion follows. This completes the proof of the lemma for X, Y = ?. For the general case: ? {?1 ? ? ? ?2} (?) (?var (? 1 , ? 2 ))(? 1 ? (?X)? ? ?) =? ? ? 2 is, due to the variable disjointness hypothesis in the lemma, ML-equivalent to the formula (?X, var (? 1 , ? 2 ))(? 1 ? ? ? ?) =? ? ? 2 , i.e., to (?X)? {?1 ? ? ? ?2} (? ? ?). To conclude the proof we apply the identity ? = (?X)?, which holds for every ML formulas ? and set X ? Var of variables (which is a simple consequence of Def. 3.9 of the ML satisfaction relation), to the two members of the equality in the lemma's conclusion

?. Hence, ?) iff ? ? ? (now interpreted as an ML formula in the signature of L) for some transition ? ? S s ? , which proves the theorem, Inria RESEARCH CENTRE LILLE ? NORD EUROPE Parc scientifique de la Haute-Borne 40 avenue Halley -Bât A -Park Plaza 59650 Villeneuve d'Ascq Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN, pp.249-6399