[. Franca, 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

F. and R. Heckmann, aiT: Worst-Case Execution Time Prediction by Static Programm Analysis, Building the Information Society. IFIP 18th World Computer Congress, pp.377-384, 2004.

A. George, W. Andrew, and . Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996.
DOI : 10.1145/229542.229546
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.4803

. Kang, Lightweight verification of separate compilation, POPL 2016: 43rd symposium on Principles of Programming Languages, pp.178-190, 2016.

P. Mccarthy, J. Mccarthy, and . Painter, Correctness of a compiler for arithmetic expressions, In Mathematical Aspects of Computer Science, vol.19, pp.33-41, 1967.
DOI : 10.1090/psapm/019/0242403

. Neis, Pilsner: a compositionally verified compiler for a higher-order imperative language, ICFP 2015: 20th International Conference on Functional Programming, pp.166-178, 2007.

. Pnueli, Translation validation, TACAS'98: Tools and Algorithms for Construction and Analysis of Systems, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

. Stewart, Compositional CompCert, POPL 2015: 42rd symposium on Principles of Programming Languages, pp.275-287, 2015.
DOI : 10.1145/2775051.2676985