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 ?

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.


Contact | Plan du site | Site réalisé avec SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1801352