The CompCert verified compiler needs all optimization passes formally verified. It lacks many optimizations found in mainstream compilers, including global value numbering (GVN). The goal of this internship is to think about how to prove correct such an optimization while minimizing proof effort and keeping the complexity of algorithms low.
Verified global value numbering
Global value numbering is kind of program optimization. How can we certify it formally at reasonable cost in both formalization and compilation time ?
