Honors and Awards

• Royal Society of Edinburgh, 2015 (Corresponding Fellow)
• VSTTE 2012 Verification Competition, Gold Medal to Team ACL2 (with Jared Davis (Centaur), Matt Kaufmann (UT), and Sol Swords (Centaur)), 2012
• National Academy of Engineering, 2007
• ACM Fellow, 2006
• ACM Software System Award, 2005 (with Robert S. Boyer and Matt Kaufmann, for the Boyer-Moore theorem prover).
• Herbrand Award, Conference on Automated Deduction (with Robert S. Boyer), 1999.
• Fellow of the Association for the Advancement of Artificial Intelligence, 1991.
• Current Prize in Automatic Theorem Proving by the American Mathematical Society (with Robert S. Boyer), 1991.
• Lecturer, Marktoberdorf International Summer School, 1988, 2002, 2004, 2008.
• John McCarthy Prize for Program Verification, 1983.
• Member of the Editorial Board of the Journal of Automated Reasoning.
• Member of the Editorial Board of Formal Methods in System Design.
• Reviewer for Mathematical Reviews.
• IBM Chaire Internationale d'Informatique, Universite de Liege, Belgium, 1980.

Return to home page.