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
January 2008. Efficient Execution in an Automated Reasoning Environment.
.2005. Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.
.2003. Inductive Assertions and Operational Semantics.
.September 1998. A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program.
.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
Contact Info
J Strother Moore
Admiral B.R. Inman Centennial Chair Emeritus in Computing Theory
(512) 471-9568