J Strother Moore

From Wikipedia, the free encyclopedia

You have new messages (last change).

J Strother Moore is a computer scientist, and is co-developer of the Boyer-Moore string search algorithm and the Boyer-Moore automated theorem prover, NQTHM. A good example of the workings of the Boyer-Moore string search algorithm is given in his website along with the Knuth-Morris-Pratt algorithm.

In addition, he is a co-author of the ACL2 automated theorem prover. Moore used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor, in the wake of the Pentium FDIV bug.

For his contributions to automated deduction he received the 1999 Herbrand Award with Robert S. Boyer.

He is currently the Chairman of the Department of Computer Sciences at The University of Texas at Austin

Before joining the Department of Computer Sciences as the chair, he formed a company Computational Logic Inc., along with others that included his close friend at the University of Texas at Austin and one of the highly regarded professors in the field of Automated Reasoning, Robert S. Boyer.

[edit] Trivia

His first name is the alphabetic character "J" – not an abbreviated "J."

Moore enjoys rock climbing.

[edit] External links

This biographical article relating to a computer specialist in the United States is a stub. You can help Wikipedia by expanding it.
This article about a US scientist is a stub. You can help Wikipedia by expanding it.
Retrieved from "http://en.wikipedia.org../../../j/_/s/J_Strother_Moore_1921.html"