J Strother Moore holds the Admiral B.R. Inman Centennial Chair 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 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. 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 Bob 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. 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.