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 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
C Chau, WA Hunt Jr, M Kaufmann, M Roncken, I Sutherland. May 15, 2018. Data-Loop-Free Self-Timed Circuit Verification. The University of Texas at Austin. Austin, Texas.
C Chau, WA Hunt, M Roncken, I Sutherland. November 13, 2017. A Framework for Asynchronous Circuit Modeling and Verification in ACL2. Haifa Verification Conference. Haifa, Israel .
Marly Roncken, Ivan Sutherland, Chris Chen, Yong Hei, Warren Hunt, Cuong Chau, Swetha Mettala Gilla, Hoon Park, Xiaoyu Song, Anping He, Hong Chen. October 29, 2017. How to think about self-timed systems. IEEE.
Luís Cruz-Filipe, Marijn JH Heule, Warren A Hunt, Matt Kaufmann, Peter Schneider-Kamp. August 6, 2017. Efficient certified RAT verification. Springer, Cham. Cham, Switzerland .
Anna Slobodova, Warren Hunt Jr. May 2, 2017. Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications. Cornell University. Ithaca, New York.
