AUSTIN, Texas— November 8, 2006, UTCS Chairman J Strother Moore was selected a Fellow of ACM, the Association for Computing Machinery.
The ACM Fellows Program was established in 1993 to recognize and honor outstanding ACM members for their achievements in computer science and information technology and for their significant contributions to the mission of the ACM. The ACM Fellows serve as distinguished colleagues to whom the ACM and its members look for guidance and leadership as the world of information technology evolves. The Fellows induction will take place on Saturday, June 9, 2007 in San Jose, California.
Professor Moore received his B.S. in Mathematics in 1970 from M.I.T. and his Ph.D. in Computational Logic from the University of Edinburgh in Scotland. He holds the Admiral B. R. Inman Centennial Chair in Computing Theory and is currently serving as Chairman of the Computer Sciences Department at The University of Texas at Austin.
In 1971, he and Robert Boyer began work on the Boyer-Moore Theorem Prover, a computer program that could discover proofs of some theorems about simple computer programs written in the programming language Lisp. The tool was designed to aid the debugging of computer hardware and software, by allowing the user to analyze mathematical models with mechanical assistance. Since 1971, the system has continued to be developed by Moore, Boyer, and Matt Kaufmann. Today it is called ACL2 and is finding use in the hardware and software industries. For their contributions to computing, Boyer, Moore, and Kaufmann won the 2005 ACM Software System Award.
ACL2, a direct descendent of The Boyer Moore Theorem Prover, has been used in industry to prove critical theorems about parts of the following commercial products:
- IBM 4758 secure co-processor
- AMD K5 microprocessor
- AMD Athlon microprocessor
- IBM Power4 microprocessor
- Motorola 68020 microprocessor
- Motorola CAP digital signal processor
- Rockwell Jem1 silicon Java Virtual Machine
- Rockwell AAMP7G cryptographic engine
- Sun JVM class loader and byte code verifier