Ken McMillan

Ken McMillan's primary research interest is in making automated formal verification tools that are usable and productive in the development of real systems, and especially in the interaction of humans and machines in formal reasoning. He is also interested in the application of concepts from automated verification to explainable AI. His past contributions to formal methods include the introduction of Symbolic Model Checking and Craig Interpolation methods, techniques that expand the scalability and range of automated verification. He worked for many years in industrial research, at AT&T Bell Labs, Cadence Research Labs, Microsoft Research, and Amazon Web Services, joining the CS faculty at UT Austin in 2021. He serves on the steering committee of the Computer-Aided Verification conference.


Research Interests: 

Ken McMillan's primary research area is formal methods. He has worked on topics such as symbolic model checking, Petri net unfoldings, automated abstraction, compositional methods, Craig interpolation, deductive verification and specification-based testing.

Select Publications

Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. Association for Computing Machinery.

McMillan K.L. (2014) Lazy Annotation Revisited. In: Biere A., Bloem R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham.

Kenneth L. McMillan, Lenore D. Zuck. 2019. Formal specification and testing of QUIC. Association for Computing Machinery.

Awards & Honors

2014 - POPL Most Influential Paper Award
2010 - LICS Test of Time Award
1998 - CMU Allen Newell Medal, CAV Award
1998 - ACM Paris Kanellakis Award
1996 - SRC Technical Excellence Award
1992 - ACM Doctoral Dissertation Award