Ken McMillan
Professor
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
Research Areas:
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
. 2018. Modularity for decidability of deductive verification with applications to distributed systems. Association for Computing Machinery.
. 2014. Lazy Annotation Revisited.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. https://doi.org/10.1007/978-3-319-08867-9_16
. 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
Contact Info
Ken McMillan
Professor, Admiral B.R. Inman Centennial Chair in Computing Theory
GDC 5.812