I received my Ph.D. from the University in December 2007.
Here is a list of my research papers.
I am most interested in developing methodologies to make the formal verification of large-scale and reconfigurable hardware designs more practical.   Formal verification has the advantage that it can check that a design satisfies its specification on all inputs, unlike testing, which can only check one input at a time (and there are far too many inputs in a large design to test every possibility).   Formal verification is, however, still impractical for large or reconfigurable designs since fully automatic techniques do not scale well and user-guided techniques are too expensive.
The approach taken in my dissertation is to increase the amount of automation available with user-guided techniques, particularly with the ACL2 theorem prover.   I have identified a decidable subclass of ACL2 formulas (SULFA), which is defined from the core primitives of the ACL2 logic and, like ACL2, is extendable with user-defined recursive functions.   I also have developed a relatively efficient SAT-based procedure for automatically verifying and finding counterexamples to SULFA formulas.   I then applied this technique to the verification of components of the TRIPS processor, a prototype next-generation processor designed and built by the University of Texas and IBM.
Note that the out-of-the-box SULFA installation requires that you be using Linux, have a Perl interpreter, a C compiler, and either zchaff (version 2007.3.12) or minisat (version 1.4 or 2) installed.   If you are interested in a different configuration, contact me at email@example.com.   It should not be hard to get SULFA to work under other operating systems or with other SAT solvers.   I have ported it to Windows in the past and my tool has a pretty simple interface for communicating with SAT solvers.