Dr. Matt Kaufmann is the co-author, with J Moore, of the ACL2 theorem
proving system.  Matt continues three decades of research and
development in support of ACL2, pursued formerly at Computational
Logic, EDS, AMD, and the University of Texas.  He received the 2005
ACM Software System Award, together with Bob Boyer and J Moore, based
on his contributions to ACL2.  Matt has authored approximately 100
publications in mathematical logic and computer science, but his
passion has been in tool development, including many industrial tools
as well as ACL2.