Matt Kaufmann began his professional career in 1978 on the mathematics
faculty at Purdue University, after receiving his Ph.D. in mathematics
at the University of Wisconsin, Madison.  In 1984 he moved to
Burroughs Corp., connecting logic (his academic research area) with
functional programming.  From 1986 until 1995 he worked at the
University of Texas and Computational Logic, Inc. on general-purpose
automated reasoning, in particular co-developing the ACL2 theorem
proving system.  Matt returned to industry in 1995: initially at
Motorola developing tools for formal hardware verification; then at
EDS with work addressing the Year 2000 problem by developing
Prolog-based program analysis tools; and finally at AMD working on
microprocessor verification, developing and employing both formal and
simulation-based techniques.  In December 2005 he took a Senior
Research Scientist position at the University of Texas (UT) at Austin
to focus his energy on research and development supporting ACL2.  He
has been continuing that work, together with J Moore, following his
formal retirement from UT in June, 2019.

Matt received the 2005 ACM Software System Award, together with Bob
Boyer and J Moore, based on his contributions to ACL2.  He has
authored approximately 100 publications in mathematical logic and
computer science, in addition to the usual academic activities (in
particular serving on Ph.D. committees, co-chairing conferences, and
reviewing papers).  But his passion has been in tool development,
especially ACL2 but also industry tools as mentioned briefly above.