Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In John Field, Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. pages 427-440, ACM, 2012. [doi]
Abstract is missing.