Kenneth McMillan Celebration
at CAV 2025

A workshop at the 37th International Conference on Computer Aided Verification

It is hardly an exaggeration to say that CAV itself might not exist without Ken's groundbreaking work on Symbolic Model Checking, Compositional Model Checking, Bounded Model Checking, Interpolation, among many others.

We gather to celebrate the many enormous contributions of Ken McMillan to the CAV and CS community. Our aim is to honor and celebrate these monumental achievements via a 1-day workshop where many of Ken's collaborators, and those inspired and influenced by his work, will present talks on these and related topics.

Workshop Date: July 22, 2025
Workshop Location: Westin Hotel Conference Center, Zagreb, Croatia

Calendar File Google Calendar Outlook Calendar Google Maps CAV 2025


Picture 1

Ken McMillan in early 2000s. From CMU Clarke Symposium 2014.

Picture 1.5

Ken McMillan in early 2000s. From CMU Clarke Symposium 2014.

Picture 2

Ken McMillan at CAV 2006. By Dennis Hamilton on Flickr.

Picture 3

Ken McMillan in Japan. From Ken McMillan's website.

Picture 4

Ken McMillan giving a talk. From POPL 2018 website.

Picture 5

Ken McMillan at ACM SIGCOMM 2019. From SIGCOMM 2019.

Picture 5

Ken McMillan's profile on UTCS website. Taken circa 2020.


Speakers

  • Aws Albarghouthi, University of Wisconsin--Madison
  • Nina Amla, National Science Foundation
  • David Dill, Stanford University
  • Asgeir Eiriksson, Apple, Inc.
  • Orna Grumberg, Technion
  • Aarti Gupta, Princeton University
  • Oded Padon, Weizmann Institute of Science
  • Lenore Zuck, University of Illinois at Chicago

Organizers

  • Ranjit Jhala, UCSD
  • Isil Dillig, UT Austin

Workshop Information

Workshop Format

This will be a 1-day workshop featuring presentations given by multiple speakers. There will be no proceedings. Further information about the presentation schedule will be posted soon.


Workshop Contact

Forthcoming


Biography of Ken McMillan

Ken McMillan is a professor at University of Texas at Austin, Austin, TX. His 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. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book “Symbolic Model Checking”, and the SMV symbolic model checking system. For his work in model checking, he has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, the Alan Newell award from Carnegie Mellon and the Computer-aided Verification Conference award.

Relevant Links

Ken McMillan's Website | Wikipedia Page | DBLP | CAV Website