Skip to main content

J Strother Moore

Professor Emeritus

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.

Research

Research Interests:
  • Automatic and machine-assisted theorem proving
    • Application to proving properties of computer hardware and software

Select Publications

J Strother Moore with D. A. Greve, M. Kaufmann, P. Manolios, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding. January 2008. Efficient Execution in an Automated Reasoning Environment.

J Strother Moore with Q. Zhang. 2005. Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.

J Strother Moore. 2003. Inductive Assertions and Operational Semantics.

J Strother Moore with T. Lynch and M. Kaufmann. September 1998. A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program.

J Strother Moore with R.S. Boyer. 1977. A Fast String Searching Algorithm.

Awards & Honors

  • 2015 - Royal Society of Edinburgh
  • 2012 - VSTTE 2012 Verification Competition, Gold Medal
  • 2007 - National Academy of Engineering,
  • 2006 - ACM Fellow
  • 2005 - ACM Software System Award
  • 1999 - Herbrand Award
  • 1991 - Fellow of the Association for the Advancement of Artificial Intelligence
  • 1991 - Current Prize in Automatic Theorem Proving by the American Mathematical Society
  • 1983 - John McCarthy Prize for Program Verification
  • 1980 - IBM Chaire Internationale d’Informatique, Universite de Liege