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