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),
- Fellow of the Association for the Advancement of Artificial
- 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.
of the Editorial Board of Formal Methods in System Design.
- Reviewer for Mathematical
- IBM Chaire Internationale
d'Informatique, Universite de Liege, Belgium, 1980.
Return to home page.