Warren A. Hunt, Jr.
Department of Computer Sciences
The University of Texas at Austin
Department of Computer Science
2317 Speedway, M/S D9500
The University of Texas
Austin, TX 78712-0233
Office: Gates Hall (GDC) 7.818
Tel: +1 512 471 9748
FAX: +1 512 471 8885
For Fall, 2013, I'm not holding regular office hours, but I'm
generally available. Please send me an E-mail to schedule an
My research involves the use of formal mathematics to write
specifications for computer hardware and software and to use proof
techniques to determine the validity of such specifications.
Specifications of both high-level intent and low-level implementations
are possible, and mechanical proof techniques can determine whether
implementations satisfy their specifications. Over the years, I have
verified a number of different microprocessor designs of increasing
I am also interested in computer architecture, low-power computing,
garbage collection, and parallel computing. Currently, I am working
specifying computer memory models.
Addtional details are available.
My primary contributions concern the formal specification and
verification of digital computing systems. I am currently involved
with X86 ISA specification and validation of SAT solvers. I also
worked briefly in the area of computational biology. I
have listed some of these
Notes and information for my
courses are on-line. I would appreciate any feedback and
My resume is available. Out of
consideration for my references, I don't include their names and
contact information on the Web, but they are available upon request.
A short biography is available.
I am working on several
research topics. Please contact me if you desire additional
I gave an invited talk at ITP
2011, about our work with Centaur Technology, Inc., where we are
verifying various properties of the 64-bit, VIA Nano, X86-compatible
I gave a talk at CAV 2009 about
my work with Sol Swords regarding our efforts at applying our tools to
VIA's Nano processor.
I was one several presenters at the CAV2004 tutorial on
microprocessor verification. I presented slides outlining the difficulty of
identifying microprocessor correctness statements, and I presented a
summary of the verification of the FM9801 (Jun Sawada's PhD
Dissertation work) as an example microprocessor verification effort.
In the second part of my presentation, I presented slides with some thoughts of what
facilities future hardware verifications system should include.
I am chairman of the FMCAD steering committee. The FMCAD conference
series has existed since 1996. The conference is supported by FMCAD,
Inc., and the conference has enjoyed "in-kind" support from the ACM
and the IEEE. For 1996 -- 2004, FMCAD conference proceeding were
published in Springer's LNCS. Since 2005, FMCAD conference papers are
available in the ACM and IEEE digital libraries. Additional details
about FMCAD are available.
Robert S. Boyer -- UTCS
Jared Davis -- PhD & Engineer.
Marijn Heule -- PhD & UTCS
Matt Kaufmann -- PhD & UTCS
Senior Research Scientist.
J Strother Moore -- UTCS
Sandip Ray -- PhD & Intel
Anna Slobodova -- PhD & Centaur
Technology Principal Engineer.
Sol Swords -- PhD & Engineer.
Tandy Warnow -- UTCS
Current PhD Students: PhD students that work in my research group.
Shilpi Goel -- CS
Robert Krug -- CS
-- CS PhD Student.
Current PhD Candidates: PhD students that have successfully
proposed and for which I am acting as their principal advisor.
Graduated PhD Students
Jun Sawada -- CS
Shant Harutunian -- ECE PhD, Spring, 2007.
Erik Reeber -- CS
PhD, Fall, 2007.
Serita Nelesen --
CS PhD, co-advised with
David Rager --
CS PhD, Fall, 2012.
Sol Swords --
CS PhD, Fall, 2010.
Ian Wehrman --
CS PhD, co-advised with
Nothing on my web pages should be taken as representing the official
position of the University of Texas at Austin or any other part of the
government of the State of Texas.
To the University of Texas at Austin Computer Sciences Department.