J. Berdine, C. Calcagno, P. W. O-'hearn, and . Smallfoot, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Lecture Notes in Computer Science, vol.4111, pp.115-137, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

S. Blazy and X. Leroy, Formal Verification of a Memory Model for C-Like Imperative Languages, ICFEM, pp.280-299, 2005.
DOI : 10.1007/11576280_20
URL : https://hal.archives-ouvertes.fr/inria-00077921

J. Filliâtre, C. Marché, and . Multi, Multi-prover Verification of C Programs, Verification of C Programs. ICFEM, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

X. Leroy, Coinductive Big-Step Operational Semantics, ESOP, pp.54-68, 2006.
DOI : 10.1006/inco.1994.1093
URL : https://hal.archives-ouvertes.fr/inria-00309010

X. Leroy, « Formal certification of a compiler back-end or : programming a compiler with a proof assistant, pp.42-54, 2006.

G. C. Necula, S. Mcpeak, and W. Weimer, type-safe retrofitting of legacy code, POPL '02 : Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.128-139, 2002.

O. 'hearn, P. W. Reynolds, J. C. Yang, and H. , « Local Reasoning about Programs that Alter Data Structures, CSL, pp.1-19, 2001.

A. Pnueli, M. Siegel, E. Singerman, and . Translation, Translation validation, TACAS, pp.151-166, 1998.
DOI : 10.1007/BFb0054170