Matt Kaufmann

Matt Kaufmann is an American computer scientist and senior research scientist at the University of Texas at Austin who, with J Strother Moore, has developed and maintained ACL2 (A Computational Logic for Applicative Common Lisp) since the early 1990s, extending the automated theorem-proving system originally designed by Robert S. Boyer and Moore. Kaufmann, Boyer and Moore received the 2005 ACM Software System Award for the Boyer-Moore theorem prover, and in 1995 Kaufmann joined Moore and Tom Lynch in using ACL2 to verify the correctness of the AMD K5 microprocessor's floating point division operation in the wake of the Pentium FDIV bug.