Kenneth L. McMillan explained

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 for 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 Bell Labs, 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

Service

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

Notes and References

  1. Web site: Ken McMillan | Department of Computer Science . Computer Science, University of Texas at Austin: Faculty and Researchers .
  2. Web site: Kenneth McMillan - The Mathematics Genealogy Project . The Mathematics Genealogy Project . American Mathematical Society (AMS) . June 21, 2023.
  3. Web site: Kenneth McMillan - ACM Awards . awards.acm.org . Association for Computing Machinery . June 21, 2023.
  4. Web site: Kenneth L. McMillan - ACM Awards . Association for Computing Machinery (ACM) - Paris Kanellakis Award . awards.acm.org . June 21, 2023.
  5. Web site: WayBackMachine - Kenneth McMillan at Microsoft Research . . https://web.archive.org/web/20190326111059/https://www.microsoft.com/en-us/research/people/kenmcmil/ . March 26, 2019. 2019-03-26 .
  6. Web site: https://twitter.com/UTCompSci/status/1365040812359176193?lang=en . Twitter . June 21, 2023.
  7. Web site: SMV Model Checker Free Download . SMV Model Checker Free Download . June 21, 2023 .
  8. Book: McMillan . K. L. . Lazy Abstraction with Interpolants . Lecture Notes in Computer Science . Computer Aided Verification . Proceedings of the International Conference on Computer Aided Verification (CAV) . 2006 . 4144 . 123–136 . 10.1007/11817963_14 . 978-3-540-37406-0 . https://link.springer.com/chapter/10.1007/11817963_14.
  9. Book: Bjorner . Nikolaj . Gurfinkel . Arie . McMillan . Ken . Rybalchenko . Andrey . Horn Clause Solvers for Software Verification . Horn Clause Solvers for Program Verification . Fields of Logic and Computation . Lecture Notes in Computer Science . 2015 . II . 24–51 . 10.1007/978-3-319-23534-9_2 . 978-3-319-23534-9 . https://link.springer.com/chapter/10.1007/978-3-319-23534-9_2.
  10. Padon . Oded . McMillan . Kenneth . Aurojit . Panda . Mooly . Sagiv . Sharon . Shoham . 2016 . 51 . 6 . Ivy: Safety verification by interactive generalization . ACM SIGPLAN Notices . 614–630 . 10.1145/2980983.2908118 .
  11. Web site: Most Influential POPL Paper Award . ACM SIGPLAN.
  12. Web site: LICS - Archive .
  13. Web site: The CMU Allen Newell Award for Research Excellence - Past Winners . Carnegie Mellon University . June 21, 2023.
  14. Web site: CAV Award . International Conference on Computer Aided Verification.
  15. Web site: Technical Excellence Award - SRC . Semiconductor Research Corporation . June 21, 2023.
  16. Web site: International Conference on Computer Aided Verification . i-cav.org . June 21, 2023.

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Kenneth L. McMillan".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.