Kenneth L. McMillan Last updated August 02, 2025 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 systems 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 References ↑ "Ken McMillan | Department of Computer Science" . Computer Science, University of Texas at Austin: Faculty and Researchers . ↑ "Kenneth McMillan - The Mathematics Genealogy Project" . The Mathematics Genealogy Project . American Mathematical Society (AMS). Retrieved June 21, 2023 . ↑ "Kenneth McMillan - ACM Awards" . awards.acm.org . Association for Computing Machinery. Retrieved June 21, 2023 . ↑ "Kenneth L. McMillan - ACM Awards" . awards.acm.org . Association for Computing Machinery (ACM) - Paris Kanellakis Award. Retrieved June 21, 2023 . ↑ "WayBackMachine - Kenneth McMillan at Microsoft Research" . Microsoft . Archived from the original on 2019-03-26. Retrieved March 26, 2019 . ↑ Computer Science at UT Austin [@UTCompSci] (Feb 25, 2021). "UTCS welcomes Professor Ken McMillan, Research Areas: Formal Methods, Programming Languages and Implementation" (Tweet ). Retrieved June 21, 2023 – via Twitter . ↑ "SMV Model Checker Free Download" . SMV Model Checker Free Download . Retrieved June 21, 2023 . ↑ McMillan, K. L. (2006). "Computer Aided Verification: Lazy Abstraction with Interpolants" . Proceedings of the International Conference on Computer Aided Verification (CAV) . Lecture Notes in Computer Science. 4144 : 123– 136. doi :10.1007/11817963_14 . ISBN 978-3-540-37406-0 . ↑ Bjorner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015). "Horn Clause Solvers for Software Verification: Horn Clause Solvers for Program Verification" . Fields of Logic and Computation . Lecture Notes in Computer Science. II : 24– 51. doi :10.1007/978-3-319-23534-9_2 . ISBN 978-3-319-23534-9 . ↑ Padon, Oded; McMillan, Kenneth; Aurojit, Panda; Mooly, Sagiv; Sharon, Shoham (2016). "Ivy: Safety verification by interactive generalization" . ACM SIGPLAN Notices . 51 (6): 614– 630. doi :10.1145/2980983.2908118 . ↑ "Most Influential POPL Paper Award" . ACM SIGPLAN. ↑ "LICS - Archive" . ↑ "The CMU Allen Newell Award for Research Excellence - Past Winners" . Carnegie Mellon University. Retrieved June 21, 2023 . ↑ "CAV Award" . International Conference on Computer Aided Verification. ↑ "Technical Excellence Award - SRC" . Semiconductor Research Corporation. Retrieved June 21, 2023 . ↑ "International Conference on Computer Aided Verification" . i-cav.org . Retrieved June 21, 2023 .
International National Academics People Other
This page is based on this
Wikipedia article Text is available under the
CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.