October 22, 2015: Distinguished Lecture - Dr. Kenneth McMillan: "Why things (don't) work: What formal methods reveal about the perversity of our designs"

Distinguished Lecture Series

Why things (don't) work: What formal methods reveal about the perversity of our designs

Dr. Kenneth McMillan
Principal Researcher at Microsoft
Thursday October 22, 2015
11:00 a.m., Room 1000 SEO Building


Things that work work for simple reasons. This bit of folk wisdom is often stated, in various forms, as a justification for our belief that the correctness of man-made systems can be mathematically proved. But is it true?? I will argue that the application of formal methods in practice reveals a more complex picture. In reality, even simple systems work for reasons that are unknown and even perverse, in the sense that no engineer would have specified these conditions explicitly. As a result, systems fail when one component is upgraded or modified. More seriously, a system that works for unknown reasons is inherently vulnerable to malicious exploitation.

This lecture will cover at a high level the compositional approach to system verification. By making assumptions about interfaces explicit, this approach often reveals not only design errors, but the unexpected reasons why things actually do work. We'll consider the implications for design practice, and how we might go about designing systems that really do work for simple reasons.


Ken McMillan is a researcher at Microsoft Research in Redmond, formerly at Cadence Berkeley Labs and Bell Labs. Beginning with his Ph.D. work at Carnegie Mellon with Ed Clarke, his research has focused on scaling automated formal verification techniques to handle real systems, particularly hardware designs. His contributions include symbolic model checking, compositional proof methodologies, and practical applications of Craig interpolation.

Host: Lenore D. Zuck

Copyright 2016 The Board of Trustees
of the University of Illinois.webmaster@cs.uic.edu
Helping Women Faculty Advance
Funded by NSF