Formally Verifying Optimizations with Block Simulations

Explore a 19-minute conference talk from OOPSLA2 2023 that delves into formally verifying compiler optimizations using block simulations. Learn how researchers from Université Grenoble Alpes - CNRS - Grenoble INP - Verimag in France have developed a framework to validate various optimizations in CompCert, an industrial-strength C compiler with mechanically checked proof of correctness. Discover how this approach enables the implementation of efficient optimizations like Lazy Code Motion and Strength Reduction while maintaining formal proofs. Gain insights into the co-design of untrusted optimizations and their validators, and understand how this method can be applied beyond CompCert. Access supplementary materials, including artifacts and a web page, to further explore the research findings and their practical applications in compiler optimization and formal verification.