Formally verified optimizing compilation in ACG-based flight control software, ERTS 2012: Embedded Real Time Software and Systems, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00653367
A precise and abstract memory model for C using symbolic values, APLAS, LNCS, vol.8858, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01093312
A concrete memory model for CompCert, ITP, LNCS, vol.9236, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01194549
A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data, Journal of Automated Reasoning, pp.1-48, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01656895
Formal verification of control-flow graph flattening, CPP. ACM, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01242063
End-to-end verification of stack-space bounds for C programs, 2014. ,
An executable formal semantics of C with applications, SIGPLAN Not, vol.47, issue.1, 2012. ,
Defining the undefinedness of C, 2015. ,
, , 1999.
A formal C memory model supporting integer-pointer casts, 2015. ,
Aliasing restrictions of C11 formalized in Coq, CPP, LNCS, vol.8307, 2013. ,
An operational and axiomatic semantics for non-determinism and sequence points in C, 2014. ,
Formal verification of a realistic compiler, C. ACM, vol.52, issue.7, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
Formal verification of a C-like memory model and its uses for verifying program transformations, Journal of Automated Reasoning, vol.41, issue.1, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00289542
Into the depths of C: elaborating the de facto standards, 2016. ,
Verified peephole optimizations for CompCert, pp.448-461, 2016. ,
C formalised in hol, 1998. ,
A formally-verified alias analysis, CPP, LNCS, vol.7679, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00773109
CompCertTSO: A verified compiler for relaxed-memory concurrency, J. ACM, vol.60, issue.3, p.50, 2013. ,