Kenneth L. McMillan
Kenneth L. McMillan , called Ken McMillan (* 20th century) is an American computer scientist who deals with model testing .
McMillan studied electrical engineering at the University of Illinois (bachelor's degree) and Stanford University (master's degree) and received his PhD in computer science from Carnegie Mellon University in 1992 under Edmund M. Clarke (Symbolic Model Checking: an approach to the state explosion problem ). There he developed his model testing system SMV. He further developed the methods at Bell Laboratories , Cadence Berkeley Labs and, from 2010, at Microsoft Research.
His method of symbolic model testing (SMV) allows the verification of logical properties of hardware or software systems with a finite number of states. He developed the tool SMV Cadence to break down complex verification problems into simpler ones. Recently he has been dealing with the relevance problem in model testing, i.e. deciding which information about a complex system is relevant in order to verify a certain logical property (using the Craig interpolation method).
In 2009 he received the Paris Kanellakis Prize for symbolic model testing with Randal Bryant , Clarke and Allen Emerson .
Web links
Individual evidence
- ↑ Kenneth L. McMillan in the Mathematics Genealogy Project (English)
| personal data | |
|---|---|
| SURNAME | McMillan, Kenneth L |
| BRIEF DESCRIPTION | American computer scientist |
| DATE OF BIRTH | 20th century |