Kenneth L. McMillan

From Infogalactic: the planetary knowledge core
Jump to: navigation, search
File:Edmund Clarke 2 FLoC 2006.jpg
Ken McMillan (middle) with David L. Dill (lower left), Robert P. Kurshan (upper left), and Edmund Clarke (right) at FLoC 2006.

Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory.[1]

Career

McMillan received his Ph.D. from Carnegie Mellon University in 1992, under Edmund M. Clarke.[2] He is credited to have invented symbolic model checking during his thesis work, which won him the 1992 ACM Doctoral Dissertation Award, the highest doctoral dissertation prize awarded by the Association of Computing Machinery (ACM).[3] He also won the 1998 ACM Paris Kanellakis Award for Theory and Practice jointly with Randal Bryant, Edmund Clarke, and E. Allen Emerson for work on symbolic model checking.[4] McMillan subsequently worked at Cadence Berkeley Labs and was a Principal Researcher at Microsoft Research, Redmond[5] before joining the faculty of University of Texas at Austin in 2021.[6]

Research

McMillan pioneered several influential research areas in formal methods. His initial work on symbolic model checking based on binary decision diagrams culminated in the creation of the SMV/nuSMV family of model checkers.[7] He also pioneered techniques based on Craig interpolation in model checking infinite-state systems.[8] He is also known for his work on Constrained Horn Clause (CHC) solving [9] and the IVy distributed system verification tool.[10]

Awards

  • 2014 - POPL Most Influential Paper Award[11]
  • 2010 - LICS Test of Time Award[12]
  • 1998 - CMU Allen Newell Medal[13]
  • 1998 - CAV Award[14]
  • 1998 - ACM Paris Kanellakis Award
  • 1996 - SRC Technical Excellence Award[15]
  • 1992 - ACM Doctoral Dissertation Award

Service

McMillan currently serves on the steering committee of the International Conference on Computer-Aided Verification (CAV).[16]

References

  1. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  2. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  3. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  4. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  5. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  6. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  7. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  8. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  9. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  10. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  11. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  12. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  13. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  14. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  15. ↑ Lua error in package.lua at line 80: module 'strict' not found.
  16. ↑ Lua error in package.lua at line 80: module 'strict' not found.
Retrieved from "https://infogalactic.com/w/index.php?title=Kenneth_L._McMillan&oldid=727039471"