TVOC: A Translation Validator for Optimizing Compilers, Computer Aided Verification, 17th Int. Conf., CAV 2005, pp.291-295, 2005. ,
DOI : 10.1007/11513988_29
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
Formal verification of dead code elimination in Isabelle/HOL, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.200-209, 2005. ,
DOI : 10.1109/SEFM.2005.20
Complete removal of redundant expressions, PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, pp.1-14, 1998. ,
A Polynomial-Time Algorithm for Global Value Numbering, Static Analysis, 11th Int. Symp., SAS 2004, pp.212-227, 2004. ,
DOI : 10.1007/978-3-540-27864-1_17
Catching and Identifying Bugs in Register Allocation, Static Analysis, 13th Int. Symp., SAS 2006, pp.281-300, 2006. ,
DOI : 10.1007/11823230_19
A PVS Based Framework for Validating Compiler Optimizations, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.108-117, 2006. ,
DOI : 10.1109/SEFM.2006.4
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
Lazy code motion, Programming Languages Design and Implementation 1992, pp.224-234, 1992. ,
Optimal code motion: theory and practice, ACM Transactions on Programming Languages and Systems, vol.16, issue.4, pp.1117-1155, 1994. ,
DOI : 10.1145/183432.183443
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
Automatically proving the correctness of compiler optimizations, Programming Language Design and Implementation 2003, pp.220-231, 2003. ,
A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, 2008. ,
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768
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
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
The CompCert verified compiler, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-01399482
Global optimization by suppression of partial redundancies, Communications of the ACM, vol.22, issue.2, pp.96-103, 1979. ,
DOI : 10.1145/359060.359069
Translation validation for an optimizing compiler, Programming Language Design and Implementation, pp.83-95, 2000. ,
The Code Validation Tool (CVT), International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.2, pp.192-201, 1998. ,
DOI : 10.1007/s100090050027
Translation validation, TACAS '98, pp.151-166, 1998. ,
DOI : 10.1007/BFb0054170
Credible compilation with pointers, Workshop on Run-Time Result Verification, 1999. ,
Symbolic transfer function-based approaches to certified compilation, 31st symposium Principles of Programming Languages, pp.1-13, 2004. ,
DOI : 10.1145/964001.964002
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.8235
Property-oriented expansion, Static Analysis, Third International Symposium, SAS'96, pp.22-41, 1996. ,
DOI : 10.1007/3-540-61739-6_31
Formal verification of translation validators: A case study on instruction scheduling optimizations, 35th symposium Principles of Programming Languages, pp.17-27, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00289540
CoVaC: Compiler Validation by Program Analysis of the Cross-Product, FM 2008: Formal Methods, 15th International Symposium on Formal Methods, pp.35-51, 2008. ,
DOI : 10.1007/978-3-540-68237-0_5
Validation of optimizing compilers, 2001. ,
VOC, Electronic Notes in Theoretical Computer Science, vol.65, issue.2, pp.223-247, 2003. ,
DOI : 10.1016/S1571-0661(04)80393-1