A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett et al., An overview of the saturn project, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering , PASTE '07, pp.43-48, 2007.
DOI : 10.1145/1251535.1251543

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

A. W. Appel and X. Leroy, A List-machine Benchmark for Mechanized Metatheory, Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP'06), pp.95-108, 2007.
DOI : 10.1016/j.entcs.2007.01.020
URL : https://hal.archives-ouvertes.fr/inria-00077531

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. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith et al., Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations, 33rd Symposium on Principles of Programming Languages, pp.55-66, 2006.

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

E. Börger, N. Fruja, V. Gervasi, and R. F. Stärk, A high-level modular definition of the semantics of <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi mathvariant="normal">C</mml:mi><mml:mo>???</mml:mo></mml:math>, Theoretical Computer Science, vol.336, issue.2-3, pp.235-284, 2005.
DOI : 10.1016/j.tcs.2004.11.008

J. Condit, M. Harren, S. Mcpeak, G. C. Necula, and W. Weimer, CCured in the real world, PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp.232-244, 2003.

D. Delahaye, C. Dubois, and J. F. Etienne, Extracting Purely Functional Contents from Logical Inductive Types, Theorem Proving in Higher Order Logics, 20th International Conference, pp.70-85, 2007.
DOI : 10.1007/978-3-540-74591-4_7
URL : https://hal.archives-ouvertes.fr/hal-01125370

T. Duff, On Duff's device URL http, 1988.

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

E. Gimenez and E. Ledinot, Semantics of a subset of the C language, 2004.

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, International Conference on Functional Programming, pp.235-246, 2002.

Y. Gurevich and J. Huggins, The semantics of the C programming language, 6th Workshop, CSL '92, pp.274-308, 1993.
DOI : 10.1007/3-540-56992-8_17

B. Hardekopf and C. Lin, The ant and the grasshopper, ACM SIGPLAN Notices, vol.42, issue.6, pp.290-299, 2007.
DOI : 10.1145/1273442.1250767

P. H. Hartel and L. Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys, vol.33, issue.4, pp.517-558, 2001.
DOI : 10.1145/503112.503115

L. Hatton, Safer language subsets: an overview and a case history, MISRA C, Information and Software Technology, vol.46, issue.7, pp.465-472, 2004.
DOI : 10.1016/j.infsof.2003.09.016

T. Hoare and P. W. O-'hearn, Separation Logic Semantics for Communicating Processes, Proceedings of the First International Conference on Foundations of Informatics, Computing and Software Electronic Notes in Computer Science, pp.3-25, 2008.
DOI : 10.1016/j.entcs.2008.04.050
URL : http://doi.org/10.1016/j.entcs.2008.04.050

M. Huisman and B. Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination, Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000, pp.284-303, 2000.
DOI : 10.1007/3-540-46428-X_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.8093

C. Hymans and O. Levillain, Newspeak, doubleplussimple minilang for goodthinkful static analysis of C. Technical note, 2008.

M. Van-inwegen, E. L. Gunter, and . Hol-ml, HOL-ML, 6th International Workshop, HUG '93, pp.61-74, 1993.
DOI : 10.1007/3-540-57826-9_125

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

D. K. Lee, K. Crary, and R. Harper, Towards a mechanized metatheory of Standard ML, 34th Symposium on Principles of Programming Languages, pp.173-184, 2007.

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), pp.2-11, 2005.
DOI : 10.1109/SEFM.2005.51

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

X. Leroy, A formally verified compiler backend URL http://gallium.inria.fr/ ? xleroy/publi/compcert-backend.pdf, 2008.

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.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0
URL : https://hal.archives-ouvertes.fr/inria-00289542

X. Leroy and H. Grall, Coinductive big-step operational semantics Information and Computation, 2007.

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The definition of Standard ML (revised), 1997.

G. C. Necula, S. Mcpeak, S. P. Rahul, and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Compiler Construction, 11th International Conference, pp.213-228, 2002.
DOI : 10.1007/3-540-45937-5_16

V. A. Nepomniaschy, I. S. Anureev, and A. V. Promsky, Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language, Programming and Computer Software, vol.29, issue.6, pp.338-350, 2003.
DOI : 10.1023/B:PACS.0000004134.24714.e5

T. Nipkow and L. C. Paulson, Isabelle/Hol: A Proof Assistant for Higher-Order Logic, 2004.
DOI : 10.1007/3-540-45949-9

M. Norrish, C formalised in HOL, 1998.

M. Norrish, Deterministic Expressions in C, Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, pp.147-161, 1999.
DOI : 10.1007/3-540-49099-X_10

S. Owens, A Sound Semantics for OCaml light, 17th European Symposium on Programming, pp.1-15, 2008.
DOI : 10.1007/978-3-540-78739-6_1

N. Papaspyrou, A formal semantics for the C programming language, 1998.

W. Paul, The Verisoft project, 2003.

N. Schirmer, Verification of sequential imperative programs in Isabelle, 2006.

K. Sen, D. Marinov, and G. Agha, CUTE: a concolic unit testing engine for C, ESEC/FSE-13: Proceedings of the 10th European software engineering conference, pp.263-272, 2005.

P. Sewell, F. Zappa-nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott: effective tool support for the working semanticist, Proceedings of the 12th International Conference on Functional Programming, pp.1-12, 2007.

M. Strecker, Compiler verification for C0, 2005.

H. Tews, Verifying Duff's device: A simple compositional denotational semantics for goto and computed jumps, 2004.

H. Tews, T. Weber, and M. Völp, A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code, Proceedings of the International Workshop on Systems Software Verification (SSV'08), pp.79-96, 2008.
DOI : 10.1016/j.entcs.2008.06.043

H. Tews, T. Weber, M. Völp, E. Poll, M. Van-eekelen et al., Nova micro-hypervisor verification. Robin project deliverable D13, 2008.

S. Zucker and K. Karhi, System V application binary interface, PowerPC processor supplement, 1995.