, Ada reference manual, 2012.

M. Barnett, M. Fähndrich, K. R. Leino, P. Müller, W. Schulte et al., Specification and Verification: The Spec# Experience, Commun. ACM, 2011.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Coq, The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, 2004.

S. Blazy and X. Leroy, Mechanized semantics for the Clight subset of the C language, Journal of Automated Reasoning, vol.43, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

D. Bruening and Q. Zhao, Practical memory checking with Dr. Memory, Annual IEEE/ACM International Symposium on Code Generation and Optimization, pp.213-223, 2011.

Y. Cheon, A runtime assertion checker for the Java Modeling Language, 2003.

L. A. Clarke and D. S. Rosenblum, A historical perspective on runtime assertion checking in software development, Software Engineering Notes, p.31, 2006.

L. Correnson and J. Signoles, Combining analyses for C program verification, Formal Methods for Industrial Case Studies (FMICS), 2012.
URL : https://hal.archives-ouvertes.fr/cea-01809014

M. Delahaye, N. Kosmatov, and J. Signoles, Common specification language for static and dynamic analysis of C programs, Symposium on Applied Computing (SAC), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00853721

P. Herms, Certification of a Tool Chain for Deductive Program Verification. (Certification d'une chaine de vérification déductive de programmes)
URL : https://hal.archives-ouvertes.fr/tel-00789543

P. Herrmann and J. Signoles, Annotation generation: Frama-C's RTE plug

. Iso/iec, Programming languages -C, vol.9899, 1999.

A. Jakobsson, N. Kosmatov, and J. Signoles, Fast as a shadow, expressive as a tree: optimized memory monitoring for C, Science of Computer Programming, vol.132, 2016.
URL : https://hal.archives-ouvertes.fr/cea-01845194

J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A Formally-Verified C Static Analyzer, SIGPLAN Not, vol.50, issue.1, pp.247-259, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01078386

R. Jung, J. H. Jourdan, R. Krebbers, and D. Dreyer, Rustbelt: Securing the foundations of the rust programming language, Proc. ACM Program. Lang, vol.2, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01633165

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.27, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

N. Kosmatov, G. Petiot, and J. Signoles, An optimized memory monitoring for runtime assertion checking of C programs, RV. LNCS, vol.8174, pp.328-333, 2013.
URL : https://hal.archives-ouvertes.fr/cea-01834990

G. T. Leavens, A. L. Baker, and C. Ruby, Preliminary design of JML: a behavioral interface specification language for java, ACM SIGSOFT Software Engineering Notes, vol.31, issue.3, pp.1-38, 2006.

H. Lehner, A Formal Definition of JML in Coq and its Application to Runtime Assertion Checking, 2011.

X. Leroy and S. Blazy, Formal verification of a C-like memory model and its uses for verifying program transformations, Journal of Automated Reasoning, vol.41, issue.1, pp.1-31, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289542

D. Ly, N. Kosmatov, F. Loulergue, and J. Signoles, Soundness of a dataflow analysis for memory monitoring, Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT), 2018.
URL : https://hal.archives-ouvertes.fr/cea-02283406

B. Meyer, Eiffel: The Language, 1991.

N. Nethercote and J. Seward, How to shadow every byte of memory used by a program, International Conference on Virtual Execution Environments, pp.65-74, 2007.

R. Rieu-helft, C. Marché, and G. Melquiond, How to Get an Efficient yet Verified Arbitrary-Precision Integer Library, Verified Software. Theories, Tools, and Experiments (VSTTE), vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732

K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov, AddressSanitizer: a fast address sanity checker, USENIX Annual Technical Conference (USENIX). USENIX Association, 2012.

J. Seward and N. Nethercote, Using Valgrind to detect undefined value errors with bit-precision, USENIX Annual Technical Conference, pp.17-30, 2005.

J. Signoles, E-ACSL: Executable ANSI/ISO C Specification Language

J. Signoles, N. Kosmatov, and K. Vorobyov, E-ACSL, a runtime verification tool for safety and security of C programs. tool paper, Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, 2017.

M. Sullivan and R. Chillarege, Software defects and their impact on system availability: a study of field failures in operating systems, Fault Tolerant Computing (FTCS), 1991.

P. N. Tollitte, D. Delahaye, and C. Dubois, Producing certified functional code from inductive specifications, Certified Programs and Proofs (CPP), pp.76-91
URL : https://hal.archives-ouvertes.fr/hal-01126212

, LNCS, 2012.

K. Vorobyov, N. Kosmatov, and J. Signoles, Detection of security vulnerabilities in C code using runtime verification: an experience report, Tests and Proofs (TAP)

. Springer, , 2018.

K. Vorobyov, J. Signoles, and N. Kosmatov, Shadow state encoding for efficient monitoring of block-level properties, International Sympoisum on Memory Management (ISMM), 2017.
URL : https://hal.archives-ouvertes.fr/cea-01836510

Z. Zhang, . Robby, J. Hatcliff, Y. Moy, and P. Courtieu, Focused Certification of an Industrial Compilation and Static Verification Toolchain, Software Engineering and Formal Methods (SEFM), vol.10469, pp.17-34, 2017.