- Computer-Aided Reasoning: An Approach, with Matt Kaufmann and Panagiotis Manolios, Kluwer Academic Publishers, 2000.
- Piton: A Mechanically Verified Assembly-Level Language, J Strother Moore, Automated Reasoning Series, Kluwer Academic Publishers, 1996.
- A Computational Logic, with Robert S. Boyer, Academic Press, 1979.
Faculty profile 2
- Member of the National Academy of Engineering
- ACM Fellow
- Fellow of the American Association for Artificial Intelligence
- ACM Software System Award, 2005
- Herbrand Award
- Current Prize in Automatic Theorem Proving by the American Mathematical Society
- Efficient Execution in an Automated Reasoning Environment, with D. A. Greve, M. Kaufmann, P. Manolios, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding, Journal of Functional Programming, 18(01), pp 15-46, January, 2008.
- Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2, with Q. Zhang, 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 373 - 384, 2005.
- Inductive Assertions and Operational Semantics, CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 289-303, 2003.
- A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program, with T. Lynch and M. Kaufmann, IEEE Transactions on Computers, 47(9), pp. 913-926, Sep., 1998.
- A Fast String Searching Algorithm, with R.S. Boyer. Communications of the Association for Computing Machinery, 20(10), 1977, pp. 762 - 772.
- Member of the Board of Directors of the Computing Research Association
- Editorial co-chair of the ACM CACM Viewpoints column
- Advisory board member of several CS departments
- Co-authored the CRA's best practices document on how university CS departments should handle intellectual property produced under industrial sponsorship
Moore does research in automatic and machine-assisted theorem proving and its application to proving properties of computer hardware and software. In essence, he builds machines that reason about machines. The theorem provers that he and his colleagues and students have built are used to verify commercial hardware and software designs - changing the very process by which designs are turned into products.