Verified Peephole Optimizations for CompCert
Mullen, Zuniga, Tatlock, Grossman
Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be eliminated by formally verifying the compiler, but state-of-theart formally verified compilers like CompCert do not support assembly-level program transformations.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!