Research

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.

Tools

We have developed a tool that uses SAT solvers to verify the Subclass of Unrollable List Formulas in ACL2 (SULFA).   As of ACL2 version 3.2, this tool is available as part of the standard ACL2 distribution.   Just download the standard acl2.tar.gz file and install it as instructed.   Then, look at the file in /books/clause-processors/SULFA/README to learn how to install and run my tool.   For a tutorial on using my tool, see the file /books/clause-processors/SULFA/books/sat-tests/tutorial.lisp

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 reeber@cs.utexas.edu.   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.

Miscellaneous

Here is a link to my personal web page.