]. W. Ahrendt, The KeY tool. Software and Systems Modeling, Bibliography, vol.4, issue.1, pp.32-54, 2005.

R. Krzysztof, . Apt, E. Frank-de-boer, and . Olderog, Verification of Sequential and Concurrent Programs, 2009.

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, Engineering Hoare Logic-Based Program Verification in K Framework, 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp.177-184, 2013.
DOI : 10.1109/SYNASC.2013.31

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 semantics for OCL. Electronic Notes in Theoretical Computer Science, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.81-96, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00998923

A. Arusoaie, T. Florin, S. , C. Ellison, and G. Ro¸suro¸su, Making Maude Definitions More Interactive, Rewriting Logic and Its Applications, 2012.
DOI : 10.1007/978-3-642-34005-5_5

I. Mariuca-asavoae, K Semantics for Abstractions, 2012.

I. Mariuca-asavoae and M. Asavoae, Collecting semantics under predicate abstraction in the K framework, WRLA, pp.123-139, 2010.

I. Mariuca-asavoae, M. Asavoae, and D. Lucanu, Path directed symbolic execution in the K framework, SYNASC, pp.133-141, 2010.

M. Asavoae, Semantics-Based WCET Analysis, 2012.

M. Asavoae, I. M. Asavoae, and D. Lucanu, On Abstractions for Timing Analysis in the $\mathbb{K}$ Framework, Proceedings of the Second International Conference on Foundational and Practical Aspects of Resource Analysis, pp.90-107, 2012.
DOI : 10.1007/978-3-642-32495-6_6

M. Irina and . As?-avoae, Abstract semantics for alias analysis in k. Electronic Notes in Theoretical Computer Science, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.97-110, 2011.

M. As?-avoae, K semantics for assembly languages: A case study Electronic Notes in Theoretical Computer Science, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.111-125, 2011.

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

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI C Specification Language (preliminary design V1.2), preliminary edition, 2008.

D. Bogd? and A. , Java semantics in K. https://github.com/ kframework/java-semantics

S. Boldo and J. Filliâtre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892

R. S. Boyer, B. Elspas, and K. N. Levitt, SELECTa formal system for testing and debugging programs by symbolic execution, Proceedings of the International Conference on Reliable Software, pp.234-245, 1975.

S. Bucur, J. Kinder, and G. Candea, Prototyping symbolic execution engines for interpreted languages, Proceedings of the 19th international conference on Architectural support for programming languages and operating systems, ASPLOS '14, pp.239-254, 2014.
DOI : 10.1145/2541940.2541977

J. Burnim and K. Sen, Heuristics for Scalable Dynamic Test Generation, 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pp.443-446, 2008.
DOI : 10.1109/ASE.2008.69

C. Cadar, D. Dunbar, and D. Engler, Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs, Proceedings of the 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 Trans. Inf. Syst. Secur, vol.12, issue.2, 2008.

V. Chipounov, V. Kuznetsov, and G. Candea, S2E, ACM SIGPLAN Notices, vol.47, issue.4, pp.265-278, 2011.
DOI : 10.1145/2248487.1950396

V. Chipounov, V. Kuznetsov, and G. Candea, The S2E Platform, ACM Transactions on Computer Systems, vol.30, issue.1, pp.1-2, 2012.
DOI : 10.1145/2110356.2110358

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.

L. A. Clarke, A program testing system, Proceedings of the annual conference on , ACM 76, pp.488-491, 1976.
DOI : 10.1145/800191.805647

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.

H. Cui, G. Hu, J. Wu, and J. Yang, Verifying systems rules using rule-directed symbolic execution, Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '13, pp.329-342, 2013.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, SEFM'12, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

J. Daniel, P. Parizek, and C. S. Pasareanu, Predicate abstraction in Java Pathfinder, ACM SIGSOFT Software Engineering Notes, vol.39, issue.1, pp.1-5, 2014.
DOI : 10.1145/2557833.2560573

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.

C. Ellison and G. Ro¸suro¸su, An executable formal semantics of C with applications, Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12), pp.533-544, 2012.

C. Ellison, T. Florin, S. , and G. Ro¸suro¸su, A Rewriting Logic Approach to Type Inference, Revised Selected Papers from the 19th International Workshop on Algebraic Development Techniques (WADT'08), pp.135-151, 2009.
DOI : 10.1007/11541868_4

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

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

R. W. Floyd, Assigning meanings to programs, of Proceedings of Symposia in Applied Mathematics, pp.19-32, 1967.
DOI : 10.1090/psapm/019/0235771

W. Gabrisch and W. Zimmermann, A Hoare-style verification calculus for control state ASMs, Proceedings of the Fifth Balkan Conference in Informatics on, BCI '12, pp.205-210
DOI : 10.1145/2371316.2371357

M. Gligoric, D. Marinov, and S. Kamin, CoDeSe, Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA '11, pp.298-308, 2011.
DOI : 10.1145/2001420.2001456

P. Godefroid, N. Klarlund, and K. Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIG- PLAN conference on Programming language design and implementation, PLDI '05, pp.213-223, 2005.

P. Godefroid, M. Y. Levin, and D. A. Molnar, SAGE, Communications of the ACM, vol.55, issue.3, pp.40-44, 2012.
DOI : 10.1145/2093548.2093564

A. Joseph, J. Goguen, and . Meseguer, Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci, vol.105, issue.2, pp.217-273, 1992.

A. Goldberg and D. Robson, Smalltalk-80: The Language and Its Implementation, 1983.

M. Gordon-andhéì-ene-collavizza, Forward with Hoare, History of Computing, pp.101-121, 2010.

K. Goshi, P. Wray, and Y. Sun, An intelligent tutoring system for teaching and learning Hoare logic, Proceedings Fourth International Conference on Computational Intelligence and Multimedia Applications. ICCIMA 2001, pp.293-297, 2001.
DOI : 10.1109/ICCIMA.2001.970482

D. Guth, A formal semantics of Python 3.3. Master's thesis, 2013.

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

M. Hills and G. Ro¸suro¸su, KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis, Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA'07), pp.246-256, 2007.
DOI : 10.1007/978-3-540-73449-9_19

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

J. Gerard and . Holzmann, The SPIN Model Checker -primer and reference manual, 2004.

W. E. Howden, Symbolic testing and the dissect symbolic evaluation system. Software Engineering, IEEE Transactions, issue.34, pp.266-278, 1977.

. Iso-iec, Standard for Programming Language C++. Working Draft

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
DOI : 10.1007/978-3-642-31424-7_61

S. Khurshid, C. S. Pasareanu, 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

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.

V. Kuznetsov, J. Kinder, S. Bucur, and G. Candea, Efficient state merging in symbolic execution, ACM SIGPLAN Notices, vol.47, issue.6, pp.193-204, 2012.
DOI : 10.1145/2345156.2254088

C. Lattner and V. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, 2004. CGO 2004., 2004.
DOI : 10.1109/CGO.2004.1281665

D. Lazar, K definition of Haskell, 2013.

D. Lazar, A. Arusoaie, C. Traian-florin-serbanuta, R. Ellison, D. Mereuta et al., Executing Formal Semantics with the $\mathbb K$ Tool, In FM LNCS, vol.7436, pp.267-271, 2012.
DOI : 10.1007/978-3-642-32759-9_23

D. Lazar and C. Ellison, K definition of the llvm assembly language, 2012.

D. Lucanu and V. Rusu, Program equivalence by circular reasoning, IFM, Lecture Notes in Computer Science, pp.362-377
DOI : 10.1007/978-3-642-38613-8_25
URL : https://hal.archives-ouvertes.fr/hal-01065830

D. Lucanu-and-traian-florin and . Serbanuta, CinK -an exercise on how to think in K, 2013.

D. Lucanu, T. Florin, S. , and G. Ro¸suro¸su, $\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

K. Ma, K. Y. Phang, J. S. Foster, and M. Hicks, Directed Symbolic Execution, Proceedings of the 18th International Conference on Static Analysis, pp.95-111, 2011.
DOI : 10.1007/3-540-45937-5_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.231.3450

K. The, Github repository. https://github

D. Daniel, E. D. Mccracken, and . Reilly, Backus-naur form (bnf), Encyclopedia of Computer Science, pp.129-131, 2003.

O. Patrick, M. Meredith, J. Katelman, G. Meseguer, and . Ro¸suro¸su, A formal executable semantics of Verilog, Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'10), pp.179-188, 2010.

J. Meseguer, Rewriting Logic and Maude: Concepts and Applications, LNCS, vol.1833, pp.1-26, 2000.
DOI : 10.1007/10721975_1

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.

J. Meseguer, Rewriting as a unified model of concurrency, CONCUR '90 Theories of Concurrency: Unification and Extension, pp.384-400, 1990.
DOI : 10.1007/BFb0039072

C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-burlet, M. R. Lowry et al., Combining unit-level symbolic execution and system-level concrete execution for testing nasa software, Proceedings of the 2008 international symposium on Software testing and analysis, ISSTA '08, pp.15-26, 2008.
DOI : 10.1145/1390630.1390635

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

C. S. Pasareanu 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. Pasareanu, W. Visser, D. H. Bushnell, J. Geldenhuys, P. C. Mehlitz et al., Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis, Automated Software Engineering, vol.10, issue.2, pp.391-425, 2013.
DOI : 10.1007/s10515-013-0122-2

G. , P. Meredith, and M. Hills, An Executable Rewriting Logic Semantics of K-Scheme, Proceedings of the 2007 Workshop on Scheme and Functional Programming (SCHEME'07), pp.91-103, 2007.

S. Person, G. Yang, N. Rungta, and S. Khurshid, Directed incremental symbolic execution, Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pp.504-515, 2011.
DOI : 10.1145/2345156.1993558
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.296.6547

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. Munoz, Rewriting modulo SMT

C. Rocha, J. Meseguer, and C. A. Munoz, Rewriting modulo SMT and open system analysis, Proceedings of the 10th International Workshop on Rewriting Techniques and Applications, WRLA'14, 2014.
DOI : 10.1016/j.jlamp.2016.10.001
URL : http://hdl.handle.net/2060/20150014338

G. Ro¸suro¸su and . Cs322, Fall 2003 -Programming Language Design: Lecture Notes, 2003.

G. Ro¸suro¸su and A. S. , Matching logic rewriting: Unifying operational and axiomatic semantics in a practical and generic framework, 2011.

G. Ro¸suro¸su, A. S. , 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¸suro¸su, 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¸suro¸su and D. Lucanu, Circular coinduction ? a proof theoretical foundation, CALCO 2009, pp.127-144, 2009.

G. Rosu, W. Schulte, and T. Serbanuta, Runtime Verification of C Memory Safety, Runtime Verification, pp.132-152, 2009.
DOI : 10.1145/248621.248623

G. Ro¸suro¸su, T. Florin, and S. , 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. Rosu and A. Stefanescu, 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¸suro¸su and A. S. , Checking reachability using matching logic, 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

G. Rosu and A. Stefanescu, 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¸suro¸su, T. Florin, S. Overview, and S. Case, <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> Overview and SIMPLE Case Study, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.3-56, 2011.
DOI : 10.1016/j.entcs.2014.05.002

S. Sapra, M. Minea, S. Chaki, A. Gurfinkel, and E. M. Clarke, Finding Errors in Python Programs Using Dynamic Symbolic Execution, ICTSS, pp.283-289, 2013.
DOI : 10.1007/978-3-642-41707-8_20

R. Sasse and J. Meseguer, Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics, Electronic Notes in Theoretical Computer Science, vol.176, issue.4, pp.29-46, 2007.
DOI : 10.1016/j.entcs.2007.06.006

P. Saxena, P. Poosankam, S. Mccamant, and D. Song, Loop-extended symbolic execution on binary programs, Proceedings of the eighteenth international symposium on Software testing and analysis, ISSTA '09, 2009.
DOI : 10.1145/1572272.1572299

K. Sen and G. Agha, CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools, Lecture Notes in Computer Science, vol.4144, pp.419-423, 2006.
DOI : 10.1007/11817963_38

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.

T. Florin and S. , A Rewriting Approach to Concurrent Programming Language Design and Semantics, 2010.

A. Traian-florin-serbanuta, D. Arusoaie, C. Lazar, D. Ellison, G. Lucanu et al., The k primer (version 3.3), Proceedings of International K Workshop ENTCS, 2013.

. Traian-florin, G. Serbanuta, and . Rosu, A truly concurrent semantics for the k framework based on graph transformations, Lecture Notes in Computer Science, vol.7562, pp.294-310, 2012.

T. Florin, S. , G. Ro¸suro¸su, and J. Meseguer, A rewriting logic approach to operational semantics, Information and Computation, vol.207, pp.305-340, 2009.

C. Zamfir and G. Candea, Execution synthesis, Proceedings of the 5th European conference on Computer systems, EuroSys '10, pp.321-334, 2010.
DOI : 10.1145/1755913.1755946

T. Florin and S. , Rewriting semantics and analysis of concurrency features for a C-like language, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.167-182, 2011.

T. Florin, S. , A. Arusoaie, D. Lazar, C. Ellison et al., The primer (version 3.3) Electronic Notes in Theoretical Computer Science, Proceedings of the Second International Workshop on the K Framework and its Applications, pp.57-80, 2011.