J. Strother and M. , A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.

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

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

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

Z. Dargaye, Décurryfication certifiée, JFLA (Journées Françaises des Langages Applicatifs), pp.119-133, 2007.

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

N. Schirmer, Verification of Sequential Imperative Programs in Isabelle, 2006.

G. Klein, H. Tuch, and M. Norrish, Types, bytes, and separation logic, POPL'07, pp.97-108, 2007.

Z. Ni and Z. Shao, Certified assembly programming with embedded code pointers, POPL'06, pp.320-333, 2006.
DOI : 10.1145/1111037.1111066

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

R. Bornat, C. Calcagno, O. Peter, M. Hearn, and . Parkinson, Permission accounting in separation logic, POPL'05, pp.259-270, 2005.

M. J. Parkinson, Local Reasoning for Java, 2005.

S. Ishtiaq, O. Peter, and . Hearn, BI as an assertion language for mutable data structures, POPL'01, pp.14-26, 2001.

O. Peter, J. Hearn, H. Reynolds, and . Yang, Local reasoning about programs that alter data structures, CSL'01, pp.1-19, 2001.

A. W. Appel, Tactics for separation logic, 2006.

T. Weber, Towards Mechanized Program Verification with Separation Logic, CSL, number 3210 in Lecture Notes in Computer Science, pp.250-264, 2004.
DOI : 10.1007/978-3-540-30124-0_21

R. Bornat, Proving Pointer Programs in Hoare Logic, MPC, pp.102-126, 2000.
DOI : 10.1007/10722010_8

J. Reynolds, 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

S. Brookes, A Grainless Semantics for Parallel Programs with Shared Mutable Data, Mathematical Foundations of Programming Semantics, 2006.
DOI : 10.1016/j.entcs.2005.11.060

A. W. Appel, A. Hobor, and F. Z. Nardelli, Oracle semantics for Concurrent C minor, 2007.

R. Affeldt, N. Marti, and A. Yonezawa, Towards formal verification of memory properties using separation logic, 22nd Workshop of the Japan Society for Software Science and Technology, 2005.

V. Domaine-de, Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche, 2004.