Proving correctness of compiler optimizations by temporal logic.

David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen

Browse the full POPL paper archive.