-
-
J S Moore II
Professor Emeritus
Department of Computer Science
Admiral B. R. Inman Centennial Chair in Computing Theory (Emeritus)Formal Methods, Security-
Ph.D,, Computational Logic, University of Edinburgh, Edinburgh, Scotland (1973)
S.B., Mathematics, Massachusetts Institute of Technology (1970)Research Interests
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.
-
Selected Publications
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.
Books:
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.
-
- 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
-
