Keynote by Microsoft

Formal methods at scale in Microsoft

Thomas Ball

Research manager, Microsoft

Today, the cost of software bugs to the global economy is manifest. For companies running global cloud platform, a single bug can result in hours of costly downtime. Microsoft Research has championed the use of formal methods for the last 15 years, deploying tools for creating reliable software based on program analysis, specification-based programming languages, and automated theorem proving.  This talk will review the research that powers Microsoft Security Risk Detection, a verified HTTPS stack and the design and implementation of highly asynchronous and distributed systems.

Thomas (Tom) Ball is a principal researcher and manager at Microsoft Research. He initiated the influential Slam software model-checking project with Sriram Rajamani, which led to the creation of the Static Driver Verifier tool for finding defects in Windows device drivers. Tom is a 2011 ACM Fellow for ‘contributions to software analysis and defect detection’. As a manager, he has nurtured research areas such as automated theorem proving, program testing/verification and empirical software engineering. His current focus is computer science education and the Microsoft Makecode platform for programming with physical computers.