Columbia COMS W4117: Compilers and Interpreters: Software Verification Tools, Fall 2007, Prof. Alfred Aho