Biography
J Strother Moore holds the Admiral B.R. Inman Centennial Chair Emeritus in
Computing Theory at the University of Texas at Austin. He is the author of
many books and papers on automated theorem proving and mechanical
verification of computing systems. Along with Robert Boyer he is a co-author
of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching
algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem
prover, which they jointly maintain and develop for use in hardware and
software verification. Moore got his BS from MIT in 1970 and his PhD from
the University of Edinburgh in 1973. Moore was a co-founder of Computational
Logic, Inc., and served as its chief scientist for ten years. He and Boyer
were awarded the Current Prize in Automatic Theorem Proving by the American
Mathematical Society in 1991 and they were awarded the Herbrand Award in
1999. In 2005, Boyer, Moore and Kaufmann won the ACM Software System Award,
for the Boyer-Moore theorem prover. Moore served as chair of the UT
Department of Computer Science from 2001 to 2009. He served on the board of
directors of the Computing Research Association for 10 years including 2
years as its chair. Moore is a Fellow of the Association for the Advancement
of Artificial Intelligence, the ACM, and the National Academy of Engineering,
and a Corresponding Fellow of the Royal Society of Edinburgh.