C. George, S. Necula, W. Mcpeak, and . Weimer, Ccured: 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.

T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney et al., Cyclone: A safe dialect of C, USENIX Annual Technical Conference, General Track, pp.275-288, 2002.

J. Filliâtre and C. Marché, Multi-prover Verification of C Programs, Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004 Proceedings, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

N. Schirmer, A Verification Environment for Sequential Imperative Programs in Isabelle/HOL, Logic for Programming, Artificial Intelligence, and Reasoning, pp.398-414, 2005.
DOI : 10.1007/978-3-540-32275-7_26

W. Peter, J. C. O-'hearn, H. Reynolds, and . Yang, Local reasoning about programs that alter data structures, Lecture Notes in Computer Science, vol.2142, pp.1-19, 2001.

J. Berdine, C. Calcagno, and P. W. Hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Lecture Notes in Computer Science, vol.4111, pp.115-137, 2005.
DOI : 10.1007/11804192_6

T. Weber, Towards Mechanized Program Verification with Separation Logic, 13th Annual Conference of the EACSL Proceedings, pp.250-264, 2004.
DOI : 10.1007/978-3-540-30124-0_21

N. Marti, R. Affeldt, and A. Yonezawa, Formal Verification of the Heap Manager of an Operating System Using Separation Logic, 8th International Conference on Formal Engineering Methods (ICFEM 2006), pp.400-419, 2006.
DOI : 10.1007/11901433_22

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), pp.97-108, 2007.

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Proc. 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06), pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

D. Leinenbach, W. Paul, and E. Petrova, Towards the formal verification of a C0 compiler: code generation and implementation correctness, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.
DOI : 10.1109/SEFM.2005.51

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

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

X. Leroy, Coinductive Big-Step Operational Semantics, Programming Languages and Systems, 15th European Symposium on Programming Proceedings, pp.54-68, 2006.
DOI : 10.1006/inco.1994.1093
URL : https://hal.archives-ouvertes.fr/inria-00309010

W. Andrew, S. Appel, and . Blazy, Separation logic for small-step Cminor, Theorem Proving in Higher Order Logics, 20th International Conference, 2007.

C. George, S. Necula, S. Mcpeak, W. Prakash-rahul, and . Weimer, CIL: Intermediate language and tools for analysis and transformation of C programs, CC '02: Proceedings of the 11th International Conference on Compiler Construction, pp.213-228, 2002.