Abstract: Autonomous driving needs machine learning, because it relies so heavily on perception. But machine learning is notoriously unpredictable and unverifiable. How then can an autonomous car ever be convincingly safe? We have been exploring the classic idea of a runtime monitor. What makes this hard is that all monitor architectures we know of either just check internal consistency properties of a controller (thus not establishing any end-to-end properties at all), or act almost as redundant “safety controllers” with their own access to sensors (which cannot work because it would require the same unverifiable complex perception that the monitor is supposed to avoid). In this talk, I’ll explain some of the ideas we’ve been toying with in an attempt to find a way out of this dilemma.

Short Bio: Daniel Jackson is a Professor of Computer Science at MIT, a MacVicar teaching fellow, and an Associate Director of the Computer Science and Artificial Intelligence Laboratory.

Dr. Jackson's research has focused primarily on software modeling and design. He is a believer in lightweight formal methods and the role of design thinking in software. Alloy, the language he developed with my students, continues to grow in popularity.

Dr. Jackson is a member of IFIP Working Group 2.3 (Programming Methodology). He received the 2016 ACM SIGSOFT Impact Award with Mandana Vaziri for their 2001 paper on verifying code with SAT, and the 2017 ACM SIGSOFT Outstanding Research Award. He is an ACM Fellow.

Dr. Jackson is also a photographer; his most recent projects are Portraits of Resilience (http://portraitsofresilience.com), and At a Distance (https://dnj.photo/projects/distance).