In 2000, Andreas Podelski visited Microsoft Research as Sriram Rajamani and I had just started the SLAM software model checking project. Andreas brought the good word about Abstract Interpretation to us, which helped us better understand the Boolean program abstraction we were creating. In my talk, I will survey the work we and Andreas did together and reflect on the many contributions to software model checking he made through the last quarter of a century.

I work in the area of programming languages and software engineering in MSR’s Redmond Lab(opens in new tab), as a member of the RiSE(opens in new tab) group. Over the past five years, I’ve turned my attention from problems plaguing professional software developers to focus on simplifying the creation of physical computing systems for the rest of society. I led the team from Microsoft that helped to deliver the BBC micro:bit(opens in new tab) to over 800,000 year-seven students in the UK, and then started Microsoft MakeCode(opens in new tab), a web-based platform to support CS education. Working with the Micro:bit Education Foundation, over nine million micro:bits have been distributed worldwide to over 60 countries. More recently, I’ve worked on Jacdac(opens in new tab), a plug-and-play system for microcontollers, and MicroCode(opens in new tab), a portable programming environment for the micro:bit.