Warren A. Hunt Jr
 | The topic of this article may not meet Wikitia's general notability guideline. |
Warren A. Hunt Jr | |
|---|---|
| Born | June 26, 1958 Mount Kisco, New York |
| Alma mater | University of Texas at Austin (Ph.D, 85 Rice University Electrical and Computer Engineering |
| Scientific career | |
| Fields | Computer science Computer architecture Formal verification |
| Institutions | University of Texas at Austin FMCAD, Inc. IBM |
| Website | https://www.cs.utexas.edu/~hunt/ |
Warren A. Hunt Jr. (born June 26, 1958) is an American computer scientist, researcher and professor at the University of Texas at Austin. His primary technical contributions concern the formalization and verification of a litany of microprocessor designs. These efforts involved specifying several microprocessor designs at the Instruction set architecture (ISA) level. Derivatives of his tools, developed on top of the ACL2 system, have been used by Advanced Micro Devices (AMD), Centaur Technology, Intel Corporation, and IBM to help assure that their microprocessor designs are correct.[1]
In 1985, Hunt was the first to mechanically verify the correctness of the FM8501 microprocessor design using a theorem-proving program.[2] In 1994, Hunt along with Bishop C. Brock specified, designed, and mechanically verified, the 32-bit FM9001, the first and only such verified microprocessor ever to be built. Their work on this was published in:The FM9001 Microprocessor:Its Formal Specification and Mechanical Correctness Proof.[3]
Hunt has been a professor at the University of Texas at Austin Computer Science department since 2002[4], where he teaches formal methods and computer architecture, and where he investigates and develops methods for microprocessor analysis and program verification,[5] automated theorem proving methods, computational biology tools, and RSFQ circuits.
Dr Hunt has been an ACM Distinguished member since 2015.
Biography
Hunt was born in Mount Kisco, New York to Sadie and Warren Alva Hunt, a physicist with a Ph.D. who spent his entire career working for IBM.
Hunt attended Rice University where he studied Electrical Engineering, concurrently satisfying the requirements for the Mathematical Science and Computer Science degree. He received his Bachelor of Science (BS) in Electrical Engineering in 1980[6], and his Doctor of Philosophy (Ph.D.) in Computer Science from the University of Texas at Austin in 1985.[7]
Hunt began working as a Research Associate at the University of Texas in Austin (UT) in 1985. In 1987, Hunt became Vice President for Hardware Engineering at Computational Logic, Inc. where he worked for 10 years. Also in 1987 he joined the department of Computer Science at UT Austin as an adjunct assistant professor. From 1992 on, he was a part-time Research Fellow in the department of Electrical and Computer Engineering, a position he held until 1997.
From 1997 to 2002, Hunt was a Research Staff Member and Manager at the Austin Research Laboratory at IBM.
From 2000 to 2019, Hunt presided over the steering committee of the FMCAD Conference Series[8], that "provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems".[9] He held the position of President of FMCAD[8], Inc., a Texas business that supported the FMCAD[8] Conference series.
in January 2005 Hunt married Anna Slobodova[10], a mathematician and Formal Verification expert, with whom he has collaborated on many projects.
Publications
- Hunt, Warren A., ed. (1994). FM8501: A Verified Microprocessor. Lecture Notes in Computer Science. Vol. 795. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-57960-5. ISBN (identifier)|ISBN 978-3-540-57960-1.[11]
- Bishop C. Brock, Warren A. Hunt Jr., and Matt Kaufmann (1994), The FM9001 Microprocessor Proof, Computational Logic, Inc, Technical Report 86, 1410 pages. Published electronically 1995.[12]
- Hunt, Warren A.; Johnson, Steven D., eds. (2000). Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1–3, 2000 Proceedings. Lecture Notes in Computer Science. Vol. 1954. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-40922-x. ISBN 978-3-540-41219-9.[13]
- Hunt, Jr., Warren A. (2002). "Introduction: Special Issue on Microprocessor Verifications", Formal Methods in System Design. 20 (2): 135–137. doi:10.1023/A:1014175712530.[14]
- Hunt, Warren A.; Somenzi, Fabio, eds. (2003). Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings. Lecture Notes in Computer Science. Vol. 2725. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/b11831. ISBN 978-3-540-40524-5.[15]
For a list of more publications see https://www.cs.utexas.edu/~hunt/vita/aug-2022.pdf
References
- ↑ Hunt, Warren A. (1 December 1989). "Microprocessor design verification". Journal of Automated Reasoning. 5 (4): 429–460. doi:10.1007/BF00243132.
- ↑ Hunt, Warren A. (1985), FM8501 : A Verified Microprocessor / Warren Alva Hunt.", University of Texas at Austin
- ↑ "TheFM9001 Microprocessor: Its Formal Specification and Mechanical Correctness Proof".
- ↑ "The University of Texas at Austin, Computer Science, College of Natural Sciences".
- ↑ Hunt, Warren. "Research Topics - Warren A Hunt Jr". Research Topics.
- ↑ "Rice University Sixty.-seventh Commencement, 1980" (PDF).
- ↑ "The University of Texas at Austin, Degrees and Dates of Attendance". The University of Texas at Austin, Degrees and Dates of Attendance.
- ↑ 8.0 8.1 8.2 "Formal Methods in Computer-Aided Design". FMCAD.
- ↑ "FMCAD". fmcad.org. Retrieved 2022-08-13.
- ↑ Slobodova, Anna. "Anna Slobodova".
- ↑ Hunt, Warren A., ed. (1994). FM8501: A Verified Microprocessor. Lecture Notes in Computer Science. Vol. 795. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-57960-5. ISBN 978-3-540-57960-1.
- ↑ Hunt Jr., Warren A (December 23, 1994). "The FM9001 Microprocessor Proof" (PDF).
- ↑ Hunt, Warren A.; Johnson, Steven D., eds. (2000). Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1–3, 2000 Proceedings. Lecture Notes in Computer Science. Vol. 1954. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-40922-x. ISBN 978-3-540-41219-9.
- ↑ Hunt, Jr., Warren A. (2002). "[No title found]". Formal Methods in System Design. 20 (2): 135–137. doi:10.1023/A:1014175712530.
- ↑ Hunt, Warren A.; Somenzi, Fabio, eds. (2003). Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings. Lecture Notes in Computer Science. Vol. 2725. Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/b11831. ISBN 978-3-540-40524-5.
External links
This article "Warren A. Hunt Jr" is from Wikipedia. The list of its authors can be seen in its historical. Articles taken from Draft Namespace on Wikipedia could be accessed on Wikipedia's Draft Namespace.