Formal verification of SSA-based optimizations for LLVM.

Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic

Browse the full PLDI paper archive.