Automated Reasoning About LLVM Optimizations and Undefined Behavior

I'm the author of this piece. Everyone should go try out Alive instead of reading the blogpost:

https://github.com/nunoplopes/alive

Alive automates all of the stuff described in the post. Here's some info:

http://blog.regehr.org/archives/1170

Also we gave a talk at the LLVM Dev meeting a few weeks ago, the talk doesn't seem to be online (yet?) but here are David's slides:

http://www.cs.utah.edu/~regehr/devconf14.pdf