
University of Texas, PhD Program, Fall 2001-Spring 2008 (expected), advisor: J Moore
University of Texas, Bachelor of Science in Electrical Engineering, 1999
Researched algorithms for automatic discovery of proofs via generalization, lemma generation, and induction for the automatic theorem proving system ACL2. Under the supervision of Professor J Moore. Fall 2001-present.
Worked at NASA JPL's LaRS on verifying a flash filesystem for the next Mars Rover. Summer 2006.
Worked at NASA Goddard on generating implementations of control systems from informal requirements. Summer 2004.