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

K. R. Apt, F. De-boer, and E. Olderog, Verification of Sequential and Concurrent Programs, 2009.

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

M. Barnett, K. R. 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

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

C. Cadar, D. Dunbar, and D. Engler, Klee: unassisted and automatic generation of highcoverage tests for complex systems programs, Proc. 8th USENIX conference on Operating systems design and implementation, OSDI'08, pp.209-224, 2008.

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.

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

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

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

L. De-moura 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?u, An executable formal semantics of C with applications, Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12), pp.533-544, 2012.

J. C. Filliâtre, Proof of the KMP string searching algorithm

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

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

D. Knuth, J. Morris, J. , and V. Pratt, Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977.
DOI : 10.1137/0206024

D. E. Knuth, J. Morris, and V. R. Pratt, Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977.
DOI : 10.1137/0206024

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

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

G. R. Patrick-meredith and M. Hills, An Executable Rewriting Logic Semantics of K-Scheme, Proceedings of the 2007 Workshop on Scheme and Functional Programming, pp.91-103, 2007.

D. A. Ramos and D. R. Engler, Practical, Low-Effort Equivalence Verification of Real Code, Proceedings of the 23rd international conference on Computer aided verification, pp.669-685, 2011.
DOI : 10.1109/32.588521

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

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 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