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

This workshop has concluded. Recorded talks may be found in the links below.

In-Person Talk Recordings Pre-recorded Messages 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

The following speakers will present in-person:

  • Aws Albarghouthi, University of Wisconsin---Madison
  • David Dill, Stanford University
  • Ásgeir Eiriksson, Apple, Inc.
  • Aarti Gupta, Princeton University
  • Daniel Kroening, Amazon
  • Kedar Namjoshi, Nokia Bell Labs
  • Oded Padon, Weizmann Institute of Science
  • Corina Păsăreanu, Carnegie Mellon University
  • Andreas Podelski, Universität Freiburg
  • Shaz Qadeer, Microsoft Research
  • Moshe Vardi, Rice University
  • Lenore Zuck, University of Illinois Chicago

The following speakers will make a pre-recorded appearance:

  • Thomas Ball, University of Washington and Lancaster University
  • Orna Grumberg, Technion
  • Andreas Kuehlmann
  • Vigyan Singhal, NVIDIA

Organizers


Workshop Chairs

  • Ranjit Jhala, UCSD
  • Işıl Dillig, UT Austin

Website and Logistics Support

  • Ruijie Fang, UT Austin

Workshop Information

Workshop Schedule

Local Time Event Details
8:30-9:00 Breakfast (provided, courtesy of CAV)
9:00-10:30 Session Welcome from Ranjit Jhala and Işıl Dillig (5 mins)
Lenore Zuck
Shaz Qadeer
Andreas Podelski
10:30-11:00 Coffee break
11:00-12:00 Session David Dill: Ken's Graduate Career video slides
Aarti Gupta: Compositional Verification of Protocol Implementations video
12:00-14:00 Lunch (provided, courtesy of CAV)
14:00-15:30 Session Ásgeir Eiriksson: Examples of Ken's Critical Contributions in Industry video
Kedar Namjoshi: Modularity + Symmetry video
Oded Padon: Duality and Primal-dual Algorithms in Verification video
15:30-16:00 Coffee break
16:00-18:00 Session Aws Albarghouthi: In Search of the Abstract video
Corina Păsăreanu: Compositional Verification of Complex Systems video
Daniel Kroening
Moshe Vardi: MoXI: An Intermediate Language to Spur Reproducible Model-Checking Research video
Speakers with Recorded Appearance
Concluding Remarks from Ken McMillan
Dinner Picture 1, Picture 2

Workshop Sponsor

Amazon Web Services


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