Formal verification of SSA-based optimizations for LLVM
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic · 2013
Modern compilers, such as LLVM and GCC, use a static single assignment(SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging because SSA properties depend on a function's entire control-flow graph.