I am a Ph.D. student in computer science at the University of Texas at Austin, in my fourth year as of spring 2008. I'm interested in mechanical theorem proving and its applications in formally verifying CPU designs. I use the ACL2 theorem prover as the basis for most of my projects. Compared to most other theorem provers, ACL2 is well suited for work in hardware verification because it emphasizes automation over logical expressivity.
ACL2 is an interesting beast. One can write programs in the ACL2 programming language (based on Common Lisp), run them like any other program, and then use the ACL2 reasoning engine to attempt to prove theorems (which are written in the same programming language) about these programs. Despite having superior automation to most other theorem provers, this process can still be quite an effort, but often it's a lot of fun. One textbook compares the process to playing a video game, and it's not far off.
I currently work at Centaur Technology on the verification effort of their newest design, the VIA Isaiah CPU architecture. (Here are some pictures from a tour of Centaur; I don't work with the fancy machinery myself, though.) My work for Centaur involves both developing verification tools based on ACL2 and applying them to components of their design in an effort to prove it correct. All of this work is in collaboration with my advisor, Warren Hunt.
- Links to better websites
- Something about my life outside of school and work
- Maybe some colors or images