C. A. Hoare, An axiomatic basis for computer programming, Comm. ACM, vol.12, issue.10, p.576580, 1969.
DOI : 10.1145/357980.358001
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

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, OOPSLA 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. Arusoaie, D. Nowak, D. Lucanu, and V. Rusu, A Certified Procedure for RLVerification, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNACS'17), 2017.

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

F. Serman and M. Hauspie, Achieving virtualization trustworthiness using software mechanisms The Tenth, International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing, 2016.
DOI : 10.1109/imis.2016.126

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. 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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.2475

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

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.

L. Moreau and J. Duprat, A construction of distributed reference counting, Acta Informatica, vol.37, issue.8, 1999.
DOI : 10.1007/PL00013315

A. E. Mccreight, The Mechanized Verification of Garbage Collector Implementations, 2008.

A. Chlipala, The bedrock structured programming system, ACM SIGPLAN Notices, vol.48, issue.9, pp.391-402, 2013.
DOI : 10.1145/2544174.2500592

B. Pierce, Software Foundations

A. Chlipala, Formal Reasoning About Programs

B. Moore and G. Rosu, Program Verification by Coinduction, 2015.

P. Barham, B. Dragovic, K. Fraser, S. Hand, T. A. Harris et al., Pratt and A. Warfield Xen and the art of virtualization, SOSP 2003, pp.164-177

E. Bugniond, S. Devine, K. Govil, and M. R. Disco, Disco: running commodity operating systems on scalable multiprocessors, ACM Transactions on Computer Systems, vol.15, issue.4, pp.412-447, 1997.
DOI : 10.1145/265924.265930

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/inria-00528590