-
-
hunt@cs.utexas.edu
Phone: 512-471-9748
Office Location
GDC 7.818
Postal Address
2317 SPEEDWAY
AUSTIN, TX 78712-
Ph.D., The University of Texas at Austin (1985)
B.S., Rice University (1980)Research Interests
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. I am also interested in computer architecture, low-power computing, garbage collection, and parallel computing.
-
Selected Publications:
"Centaur Technology Media Unit Verification," with Sol O. Swords, in the 20th Computer-Aidied Verification Conference (CAV 2009), Lecture Notes in Computer Science (LNCS), No. 5643, pp~353--367, Springer-Verlag, June, 2009.
"A Mechanical Analysis of Program Verification Strategies'', with John Matthews, J Strother Moore, and Sandip Ray, in Journal of Automated Reasoning, Springer-Verlag, Volume 40, Number 4, pages 245-269, May, 2008.
"A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance," with Robert S. Boyer and Serita M. Nelesen in Algorithms in Bioinformatics: 5th International Workshop (WABI 2005), Lecture Notes in Computer Science, No. 3692, pp.~353--364, Springer-Verlag, 2005.
"Verifying the FM9801 Microarchitecture,'' with Jun Sawada, in IEEE Micro, IEEE Press, pp.~47--55, May-June, 1999.
"The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor," with Bishop C. Brock, in Formal Methods in Systems Design, Volume 11, pp.~71--105, Kluwer Academic Publishers, 1997.
Books:
"Computer-Aided Verification," with Fabio Somenzi (editors), LNCS 2725, Springer-Verlag, 2003.
The Commercial Use of Formal Verification, (co-editor with Ganesh Gopalakrishnan) special issue of "Formal Methods in Systems Design," Kluwer Academic Publishers, Volume 21, Number 2, March 2003.
Microprocessor Verification, (editor) special issue of "Formal Methods in Systems Design," Kluwer Academic Publishers, Volume 20, Number 2, March, 2002.
"Formal Methods in Computer-Aided Design," with Steven D. Johnson (editors), LNCS 1954, Springer-Verlag, 2000.
A Verified Microprocessor, LNAI Number 795, Springer-Verlag, 1994.
-
