A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs, pp.5-21, 2007.
DOI : 10.1007/978-3-540-74591-4_3
URL : https://hal.archives-ouvertes.fr/inria-00165915

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

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

R. Bornat, Proving Pointer Programs in Hoare Logic, MPC '00: Proc. Int. Conf. on Mathematics of Program Construction, pp.102-126, 2000.
DOI : 10.1007/10722010_8

R. Burstall, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, vol.7, pp.23-50, 1972.

?. Chrz and J. Aszcz, Modules in type theory with generative definitions, 2004.

S. Conchon, E. Contejean, and J. Kanig, The Ergo automatic theorem prover. Software and documentation available at http://ergo.lri.fr, 2005.

D. Moura, L. Bjørner, and N. , Z3: an efficient SMT solver. Software and documentation available at http://research.microsoft.com/projects, p.3, 2006.

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

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

J. C. Filliâtre, C. Marché, Y. Moy, and T. Hubert, The Why software verification platform. Software and documentation available at http://why.lri.fr, 2004.

L. Jia and D. Walker, ILC: A Foundation for Automated Reasoning About Pointer Programs, 15th European Symposium on Programming, pp.131-145, 2006.
DOI : 10.1007/978-3-540-30557-6_8

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symposium Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. Manson, W. Pugh, and S. V. Adve, The Java memory model, 32nd symposium Principles of Programming Languages, pp.378-391, 2005.

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

A. Mccreight, Z. Shao, C. Lin, and L. Li, A general framework for certifying garbage collectors and their mutators. In: Programming Language Design and Implementation, pp.468-479, 2007.

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, Information and Computation, vol.199, issue.1-2, pp.200-227, 2005.
DOI : 10.1016/j.ic.2004.10.007

M. Nita, D. Grossman, and C. Chambers, A theory of platform-dependent low-level software. In: 35th symposium Principles of Programming Languages, 2008.

M. Norrish, C formalized in HOL, 1998.

O. 'hearn, P. W. Reynolds, J. C. Yang, and H. , Local reasoning about programs that alter data structures, Computer Science Logic, 15th Int. Workshop, CSL 2001, pp.1-19, 2001.

J. C. Reynolds, Intuitionistic reasoning about shared data structures, Millenial Perspectives in Computer Science, pp.303-321, 2000.

J. C. 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

X. Shen, R. Arvind, and L. , Commit-reconcile & fences (CRF), ISCA '99: Proc. int. symp. on Computer Architecture, pp.150-161, 1999.
DOI : 10.1145/307338.300992

R. D. Tennent and D. R. Ghica, Abstract models of storage, Higher-Order and Symbolic Computation, pp.119-129, 2000.

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, 34th symposium Principles of Programming Languages, pp.97-108, 2007.
DOI : 10.1145/1190215.1190234
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.461.5649

Y. Yang, G. Gopalakrishnan, and G. Lindstrom, UMM: an operational memory model specification framework with integrated model checking capability, Concurrency and Computation: Practice and Experience, vol.48, issue.5-6, pp.5-6, 2005.
DOI : 10.1002/cpe.837