J Strother Moore

In addition, Moore is a co-author of the ACL2 automated theorem prover and its predecessors including Nqthm, for which he received, with Robert S. Boyer and Matt Kaufmann, the 2005 ACM Software System Award. He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.

For his contributions to automated deduction, Moore received the 1999 Herbrand Award with Robert S. Boyer, and in 2006 he was inducted as a Fellow in the Association for Computing Machinery. Moore was elected a member of the National Academy of Engineering in 2007 for contributions to automated reasoning about computing systems. He is also a Fellow of the AAAI. He was elected a Corresponding Fellow of the Royal Society of Edinburgh in 2015.

He is currently the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin, and was chair of the Department of Computer Science from 2001 to 2009.

Before joining the Department of Computer Sciences as the chair, he formed a company, Computational Logic Inc., along with others including his close friend at the University of Texas at Austin and one of the highly regarded professors in the field of automated reasoning, Robert S. Boyer.

Moore enjoys rock climbing.