The KeY tool. Software and Systems Modeling, pp.32-54, 2005. ,
Verification of Sequential and Concurrent Programs, 2009. ,
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
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
Java semantics in K. https://github.com/kframework/java-semantics ,
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. ,
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. ,
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
Introduction to Algorithms, 2001. ,
Verifying systems rules using rule-directed symbolic execution, ACM SIGPLAN Notices, vol.48, issue.4, pp.329-342, 2013. ,
DOI : 10.1145/2499368.2451152
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. ,
An executable formal semantics of C with applications, Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12), pp.533-544, 2012. ,
Proof of the KMP string searching algorithm ,
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
Dynamic logic, Handbook of Philosophical Logic, pp.497-604, 1984. ,
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
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
Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977. ,
DOI : 10.1137/0206024
Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977. ,
DOI : 10.1137/0206024
CinK -an exercise on how to think in K, 2013. ,
Rewriting Logic and Maude: Concepts and Applications, LNCS, vol.1833, pp.1-26, 2000. ,
DOI : 10.1007/10721975_1
An Executable Rewriting Logic Semantics of K-Scheme, Proceedings of the 2007 Workshop on Scheme and Functional Programming, pp.91-103, 2007. ,
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
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
One-path reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013. ,
Circular Coinduction: A Proof Theoretical Foundation, CALCO 2009, pp.127-144, 2009. ,
DOI : 10.1007/978-3-540-73859-6_25
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