Kenneth L. McMillan

Kenneth L. McMillan, genannt Ken McMillan (* 20. Jahrhundert) ist ein US-amerikanischer Informatiker, der sich mit Modellprüfung befasst.

McMillan studierte Elektrotechnik an der University of Illinois (Bachelor-Abschluss) und der Stanford University (Master-Abschluss) und wurde 1992 bei Edmund M. Clarke in Informatik an der Carnegie Mellon University promoviert (Symbolic Model Checking: an approach to the state explosion problem). Dort entwickelte er sein Modellprüfungssystem SMV. Er entwickelte die Methoden weiter bei den Bell Laboratories, den Cadence Berkeley Labs und ab 2010 bei Microsoft Research.

Seine Methode der Symbolischen Modellprüfung (SMV) erlaubt die Verifikation logischer Eigenschaften von Hard- oder Software-Systemen mit endlich vielen Zuständen. Er entwickelte das Tool SMV Cadence zur Zerlegung komplexer Verifikationsprobleme in einfachere. In jüngster Zeit befasst er sich mit dem Relevanz-Problem in der Modellprüfung, das heißt zu entscheiden welche Informationen über ein komplexes System relevant sind um eine bestimmte logische Eigenschaft zu verifizieren (mit der Methode der Craig Interpolation).

2009 erhielt er mit Randal Bryant, Clarke und Allen Emerson den Paris-Kanellakis-Preis für Symbolische Modellprüfung.