A. Armando, M. Benerecetti, and J. Mantovani, Model Checking Linear Programs with Arrays, Proceedings of the Workshop on Software Model Checking, 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, Towards a <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd" xmlns:sa="http://www.elsevier.com/xml/common/struct-aff/dtd"><mml:mi mathvariant="double-struck">K</mml:mi></mml:math> Semantics for OCL, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.81-96, 2011.
DOI : 10.1016/j.entcs.2014.05.004

A. Arusoaie, D. Lucanu, V. Rusu, T. F. Serbanuta, A. Stefanescu et al., Language Definitions as Rewrite Theories, Proceedings of the 10th International Workshop on Rewriting Logic and its Applications (WRLA'14), pp.97-112, 2014.
DOI : 10.1007/978-3-319-12904-4_5
URL : https://hal.archives-ouvertes.fr/hal-00950775

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

J. Berdine, C. Calcagno, and P. W. O-'hearn, Symbolic Execution with Separation Logic, APLAS, pp.52-68, 2005.
DOI : 10.1007/11575467_5

D. Bogd?na?, G. Ro?u, and . Java, A Complete Semantics of Java, Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15, 2015.

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.

M. Clavel, F. Durán, S. Eker, J. Meseguer, P. Lincoln et al., All About Maude, A High-Performance Logical Framework, LNCS, vol.4350, 2007.

J. De-halleux and N. Tillmann, Parameterized Unit Testing with Pex, Lecture Notes in Computer Science, vol.4966, pp.171-181, 2008.
DOI : 10.1007/978-3-540-79124-9_12

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Lecture Notes in Computer Science, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

L. K. Dillon, Verifying general safety properties of Ada tasking programs, IEEE Transactions on Software Engineering, vol.16, issue.1, pp.51-63, 1990.
DOI : 10.1109/32.44363

C. Ellison and G. Rosu, An executable formal semantics of C with applications, ACM SIGPLAN Notices, vol.47, issue.1, pp.533-544, 2012.
DOI : 10.1145/2103621.2103719

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
URL : http://doi.org/10.1016/j.entcs.2009.05.015

D. Filaretti and S. Maffeis, An Executable Formal Semantics of PHP, Proceedings of European Conference on Object-Oriented Programming, 2014.
DOI : 10.1007/978-3-662-44202-9_23

P. Godefroid, N. Klarlund, and K. Sen, DART: directed automated random testing, PLDI, pp.213-223, 2005.

M. Hills and G. Rosu, KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis, RTA, pp.246-256, 2007.
DOI : 10.1007/978-3-540-73449-9_19

S. Khurshid, C. S. P?s?reanu, and W. Visser, Generalized Symbolic Execution for Model Checking and Testing, TACAS, pp.553-568, 2003.
DOI : 10.1007/3-540-36577-X_40

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

G. Li, I. Ghosh, and S. P. Rajan, KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs, Lecture Notes in Computer Science, vol.6806, pp.609-615, 2011.
DOI : 10.1007/978-3-642-00768-2_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.205.5180

D. Lucanu, V. Rusu, A. Arusoaie, and D. Nowak, Verifying reachabilitylogic properties on rewriting-logic specifications. Logic, Rewriting, and Concurrency -Festschrift Symposium in Honor of José Meseguer, to appear . Also available as a technical report http
DOI : 10.1007/978-3-319-23165-5_21
URL : https://hal.archives-ouvertes.fr/hal-01158941

D. Lucanu, T. F. ?erb?nu??, and G. Ro?u, $\mathbb{K}$ Framework Distilled, 9th International Workshop on Rewriting Logic and its Applications, pp.31-53, 2012.
DOI : 10.1007/978-3-642-34005-5_3

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.

C. S. P?s?reanu and W. Visser, Verification of Java Programs Using Symbolic Execution and Invariant Generation, Lecture Notes in Computer Science, 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

C. Rocha, J. Meseguer, and C. A. Muñoz, Rewriting Modulo SMT and Open System Analysis, Lecture Notes in Computer Science, vol.8663, pp.247-262, 2014.
DOI : 10.1007/978-3-319-12904-4_14
URL : http://hdl.handle.net/2060/20150014338

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 T. F. ?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, OOPSLA, pp.555-574, 2012.

G. Rosu and A. Stefanescu, 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

D. Sannella and A. Tarlecki, Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science . An EATCS Series, 2012.

P. H. Schmitt and B. Weiß, Inferring invariants by symbolic execution, Proceedings of 4th International Verification Workshop (VERIFY'07), 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, pp.263-272, 2005.

T. ?erb?nu??, G. Ro?u, and J. 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

S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke, Using model checking with symbolic execution to verify parallel numerical programs, Proceedings of the 2006 international symposium on Software testing and analysis , ISSTA'06, pp.157-168, 2006.
DOI : 10.1145/1146238.1146256

M. Staats and C. S. P?s?reanu, Parallel symbolic execution for structural test generation, Proceedings of the 19th international symposium on Software testing and analysis, ISSTA '10, pp.183-194, 2010.
DOI : 10.1145/1831708.1831732