Biography:

J Strother Moore, professor emeritus at the University of Texas at Austin,
held the Admiral B.R. Inman Centennial Chair in Computing Theory until his
retirement in 2015.  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.  Boyer and Moore also invented the ``piece
table'' data structure underlying Microsoft Word and a linear-time majority
vote algorithm.  With Matt Kaufmann he is the co-author of the ACL2 theorem
prover.  Moore got his SB from MIT in 1970 and his PhD from the University of
Edinburgh in 1973.  Moore was a founder of Computational Logic, Inc., and
served as its Chief Scientist for ten years.  He served as chair of the UT
Austin CS department from 2001-09 and led the $120M drive to build the Bill &
Melinda Gates Center for Computer Science and the Dell Computer Science Hall,
opened in April, 2013.  He and Bob Boyer were awarded the McCarthy Prize in
1983 and the Current Prize in Automatic Theorem Proving by the American
Mathematical Society in 1991.  In 1999, they were awarded the Herbrand Award
for their work in automatic theorem proving.  Boyer, Moore, and Kaufmann were
awarded the 2005 ACM Software Systems Award for the Boyer-Moore theorem
prover.  Moore is a Fellow of Association for the Advancement of Artificial
Intelligence, the ACM, the Royal Society of Edinburgh (Corresponding Fellow)
and the US National Academy of Engineering.