Ken McMillan, a professor in the Department of Computer Science, was recently inducted into the National Academy of Engineering, one of the highest honors in the field. McMillan is known for his work on symbolic model checking, which enabled automatic verification of hardware and software systems with extremely large state spaces. His innovations laid the foundation for tools such as the Symbolic Model Verifier (SMV), which have become essential for ensuring correctness in complex engineering systems.
McMillan’s research also advanced techniques such as Craig interpolation and constraint solving in verification, influencing modern verification tools across industries and research. McMillan’s foundational work now supports both hardware verification and emerging research in explainable artificial intelligence, connecting logic with machine learning.
Before joining the UTCS faculty in 2021, McMillan worked in a wide range of industry settings, including at AT&T Bell Labs, Cadence Research Labs, Microsoft Research and Amazon Web Services.
This year, NAE elected a total of 130 new members and 28 international members. Election to the academy is among the highest professional distinctions bestowed upon an engineer. Membership honors those who have made outstanding contributions to engineering research and practice, including pioneering new and developing fields of technology and making significant advancements in the engineering field and profession.
Learn more about the newest Longhorn NAE members and their immense contributions to their fields.