Jump to content

Draft:Warren A. Hunt Jr

From Wikipedia, the free encyclopedia
  • Comment: He has certainly had a strong career. However, as written this article does not prove notability, please see WP:NPROF. With a relatively modest h-factor of 32 and no major awards (not grants), the evidence is not there. If there are notability demonstrations, e.g. newspaper interviews, these need to be in.
    The long list of his papers is not useful, please cut to 5 or just use those already in the ref.
    He might be notable, but you have to prove it. Ldm1954 (talk) 13:33, 20 January 2024 (UTC)
  • Comment: Put the lists of publications in chronological order, oldest first. Currently the oldest are last, which is not appropriate for an encyclopedia article. You can use his CV at https://www.cs.utexas.edu/~hunt/vita/aug-2022.pdf as a reference for his education and employment history. Do not put external links in the article as you did to link to Computational Logic. See WP:EXTERNAL for an explanation. StarryGrandma (talk) 01:22, 13 January 2024 (UTC)

Warren A. Hunt Jr
File:Warren-A-Hunt-2022-1.jpg
Hunt in 2022
Born (1958-06-26) June 26, 1958 (age 65)
Mt. Kisco, New York, United States
Alma materUniversity of Texas at Austin (Ph.D, 85
Rice University (B.S., 1980)
Scientific career
FieldsComputer science
Computer architecture
Formal Verification
InstitutionsUniversity of Texas at Austin
FMCAD, Inc.
IBM Corporation
ForrestHunt, Inc.
Websitehttps://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]

Much of Hunt's work is concerned with using or developing the ACL2 theorem proving system. Since 2020, Hunt has been collaborating with Ivan Sutherland on rapid single-flux quantum (RSFQ) logic. This effort concerns developing a methodology to specify, design, model, validate, verify, build, test, and analyze RSFQ logic circuits, working closely with scientists at MIT Lincoln Laboratory (MTI/LL), where there are other scientists investigating the properties of such circuits.

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[edit]

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[edit]

  • 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.[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[edit]

  1. ^ Hunt, Warren A. (1 December 1989). "Microprocessor design verification". Journal of Automated Reasoning. 5 (4): 429–460. doi:10.1007/BF00243132. S2CID 34775606.
  2. ^ Hunt, Warren A. (1985), FM8501 : A Verified Microprocessor / Warren Alva Hunt.", University of Texas at Austin
  3. ^ "TheFM9001 Microprocessor: Its Formal Specification and Mechanical Correctness Proof".
  4. ^ "The University of Texas at Austin, Computer Science, College of Natural Sciences".
  5. ^ Hunt, Warren. "Research Topics - Warren A Hunt Jr". Research Topics.
  6. ^ "Rice University Sixty.-seventh Commencement, 1980" (PDF).
  7. ^ "The University of Texas at Austin, Degrees and Dates of Attendance". The University of Texas at Austin, Degrees and Dates of Attendance.
  8. ^ a b c "Formal Methods in Computer-Aided Design". FMCAD.
  9. ^ "FMCAD". fmcad.org. Retrieved 2022-08-13.
  10. ^ Slobodova, Anna. "Anna Slobodova".
  11. ^ 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. S2CID 9838058.
  12. ^ Hunt Jr., Warren A (December 23, 1994). "The FM9001 Microprocessor Proof" (PDF).
  13. ^ 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. hdl:1807/32762. ISBN 978-3-540-41219-9. S2CID 6465963.
  14. ^ Hunt, Jr., Warren A. (2002). "[No title found]". Formal Methods in System Design. 20 (2): 135–137. doi:10.1023/A:1014175712530. S2CID 207635357.
  15. ^ 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. S2CID 221286283.

External links[edit]