Z. Manna and A. , Pnueli The temporal logic of reactive and concurrent systems specification, 1992.

G. Ro¸suro¸su and A. , Towards a unified theory of operational and axiomatic semantics, ICALP 2012, Springer LNCS 7392, pp.351-363

G. Ro¸suro¸su and A. , Checking reachability using matching logic, OOP- SLA 2012, pp.555-574

G. Ro¸suro¸su, A. , S. ¸. Ciobâc?, and B. Moore, One-path reachability logic, LICS 2013, pp.358-367

A. , S. ¸. Ciobâc?-a, R. Mereut¸?mereut¸?-a, B. Moore, T. F. et al., All-path reachability logic, RTA 2014, pp.425-440

A. S. ¸tef?-anescu, D. Park, S. Yuwen, Y. Li, and G. Ro¸suro¸su, Semantics-based program verifiers for all languages, OOPSLA'16, pp.74-91

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, Springer LNCS 9200, pp.451-474
DOI : 10.1007/978-3-319-12904-4_5
URL : https://hal.archives-ouvertes.fr/hal-01158941

S. Skeirik, A. Stefanescu, and J. Meseguer, A constructor-based reachability logic for rewrite theories, 2017.

G. Lowe, Breaking and fixing the needham-schroeder public-key protocol using FDR. Software -Concepts and Tools, pp.93-102, 1996.
DOI : 10.1007/3-540-61042-1_43
URL : http://www.cs.ubc.ca/~ajh/courses/cpsc513/NSFDR.ps

G. Ro¸suro¸su, Matching logic, RTA 2015, pp.5-21

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

J. Jaffar, V. Murali, J. Navas, and A. Santosa, TRACER: A Symbolic Execution Tool for Verification, CAV, 2012, Springer LNCS 7358, pp.758-766
DOI : 10.1007/978-3-642-31424-7_61
URL : http://www.comp.nus.edu.sg/%7Ejoxan/papers/tracer.pdf

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://www.elet.polimi.it/Users/DEI/Sections/Compeng/Giovanni.Denaro/papers/ESEC-FSE2001.pdf

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.

K. Sen, D. Marinov, and G. Agha, CUTE: a concolic unit testing engine for C, ESEC/FSE 2005, ACM, pp.263-272
DOI : 10.21236/ada482657

C. and N. Rungta, Symbolic PathFinder: symbolic execution of Java bytecode, ASE 2010, pp.179-180

D. Lucanu, V. Rusu, and A. Arusoaie, A generic framework for symbolic execution: A coinductive approach, Journal of Symbolic Computation, vol.80, pp.125-163, 2017.
DOI : 10.1016/j.jsc.2016.07.012
URL : https://hal.archives-ouvertes.fr/hal-01238696

C. Rocha, J. Meseguer, and C. Muñoz, Rewriting modulo SMT and open system analysis, Journal of Logical and Algebraic Methods in Programming, vol.86, issue.1, pp.269-297, 2017.
DOI : 10.1016/j.jlamp.2016.10.001

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

K. Bae, S. Escobar, and J. Meseguer, Abstract Logical Model Checking of Infinite- State Systems Using Narrowing, LIPICS, vol.21, pp.81-96, 2013.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-00930103