, Advanced Lectures, chap. Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency, Formal Methods for Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, pp.263-309, 2014.
, A Generic Framework for Symbolic Execution: Theory and Applications, Inria, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00766220
, Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237
, Let's verify this with Why3, International Journal on Software Tools for Technology Transfer (STTT), vol.17, issue.6, pp.709-727, 2015.
, Deductive verification with ghost monitors, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926659
, Lightweight interactive proving inside an automatic program verifier, Proceedings of the Fourth Workshop on Formal Integrated Development Environment, F-IDE, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01936302
, The spirit of ghost code, Formal Methods in System Design, vol.48, issue.3, pp.152-174, 2016.
, A Formally Verified Interpreter for a Shelllike Programming Language, VSTTE 2017 -9th Working Conference on Verified Software: Theories, Tools, and Experiments, vol.10712, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01534747
, Deciding the first-order theory of an algebra of feature trees with updates, International Joint Conference on Automated Reasoning, pp.439-454, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01807474
, A formally-verified C static analyzer, 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.247-259, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01078386
,
, The formal semantics of programming languages: an introduction, 1993.