AbsInt Advanced Analyzer for PowerPC, 2015. ,
Formal Verification of an SSA-Based Middle-End for CompCert, ACM Transactions on Programming Languages and Systems, vol.36, issue.1, p.4, 2014. ,
DOI : 10.1145/2579080
URL : https://hal.archives-ouvertes.fr/hal-01097677
Formally verified optimizing compilation in ACG-based flight control software, ERTS 2012: Embedded Real Time Software and Systems, 2012. ,
Standard ECMA-404 The JSON Data Interchange Format, 2013. ,
Volatiles are miscompiled, and what to do about it, Proceedings of the 7th ACM international conference on Embedded software, EMSOFT '08, pp.255-264, 2008. ,
DOI : 10.1145/1450058.1450093
aiT: Worst-Case Execution Time Prediction by Static Program Analysis, Building the Information Society. IFIP 18th World Computer Congress, pp.377-384, 2004. ,
DOI : 10.1007/978-1-4020-8157-6_29
Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996. ,
DOI : 10.1145/229542.229546
Validating LR(1) Parsers, ESOP 2012: 21st European Symposium on Programming, pp.397-416, 2012. ,
DOI : 10.1007/978-3-642-28869-2_20
URL : https://hal.archives-ouvertes.fr/hal-01077321
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
Translation validation. In TACAS'98: Tools and Algorithms for Construction and Analysis of Systems, LNCS, vol.1384, pp.151-166, 1998. ,
Finding and understanding bugs in C compilers, PLDI '11, pp.283-294, 2011. ,
Formal verification of SSA-based optimizations for LLVM, PLDI'13: ACM SIG- PLAN Conference on Programming Language Design and Implementation, pp.175-186, 2013. ,