Robert S. Boyer
Robert S. Boyer researches automated reasoning and program verification. His shared theorem-prover work includes Nqthm and the ACL2 family. Boyer was a research fellow at Edinburgh from 1971 to 1973 and worked at SRI from 1973 to 1981. These appointments preceded his Texas faculty career. Boyer and J Strother Moore joined the Texas computer-science faculty in 1981. Their Nqthm theorem prover became a major part of its program-verification research. Boyer, Moore and Matt Kaufmann received the 2005 ACM Software System Award for their theorem-prover software. Their software supports mechanical proof and verification of hardware and programs.
- Works
- 86
- Citations
- 5,699
- h-index
- 26
Publication numbers from OpenAlex, as of 14 October 2026.
Timeline
-
1971–1981
Automated-reasoning career
Boyer was a research fellow at Edinburgh from 1971 to 1973 and worked at SRI from 1973 to 1981. These appointments preceded his Texas faculty career.
-
1981
Texas theorem-proving research
Boyer and J Strother Moore joined the Texas computer-science faculty in 1981. Their Nqthm theorem prover became a major part of its program-verification research.
-
2005
Shared software award
Boyer, Moore and Matt Kaufmann received the 2005 ACM Software System Award for their theorem-prover software. Their software supports mechanical proof and verification of hardware and programs.
-
2008
Emeritus appointment
Boyer became emeritus at Texas in 2008, after faculty service from 1981 to 2008.
Sources and credits
Photo: cs.utexas.edu; Home page of Robert S. Boyer; creator not stated. License: Not stated by source. Source: cs.utexas.edu. Cropped to a square and resized. Ask us to remove or replace this photo.