J Strother Moore
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