Warren Hunt Jr.
Professor
Warren Hunt Jr. teaches formal methods and computer architecture. He is currently investigating and developing methods for microprocessor specification and program verification, automated theorem-proving methods, and computational biology tools. He has been active in the hardware verification area for more than 25 years, and has applied formal verification tools and methods to a litany of microprocessor designs, completing the first complete mechanical verification of a microprocessor design in 1985. Outside of research, he also serves as an associate editor for the "Formal Methods in System Design" journal.
Research
Research Areas:
Research Interests:
- X86 Specification in ACL2
- Hash CONS
- Function Memoization
- Fast Association Lists
- Formal Hardware Description Languages
- TASPI
- Integration of ACL2 and HOL4
- Transistor-level Circuit Analysis
- Verification of Control Systems
- Improved Arithmetic Procedures for ACL2
Select Publications
. May 15, 2018. Data-Loop-Free Self-Timed Circuit Verification. The University of Texas at Austin. Austin, Texas.
. November 13, 2017. A Framework for Asynchronous Circuit Modeling and Verification in ACL2. Haifa Verification Conference. Haifa, Israel .
. October 29, 2017. How to think about self-timed systems. IEEE.
. August 6, 2017. Efficient certified RAT verification. Springer, Cham. Cham, Switzerland .
. May 2, 2017. Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications. Cornell University. Ithaca, New York.
Contact Info
Warren Hunt Jr.
Professor
(512) 471-9748
GDC 5.826
M 11AM - 1 PM. W 11AM - 11:45AM