Kenneth L. McMillan

Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages.

[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.

[8] He is also known for his work on Constrained Horn Clause (CHC) solving[9] and the IVy distributed system verification tool.

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

Ken McMillan (middle) with David L. Dill (lower left), Robert P. Kurshan (upper left), and Edmund Clarke (right) at FLoC 2006.