Abstract

What do the topics of data center configuration, device drivers, cryptography, message parsers and protocols have in common? In three words: logic and languages! In this talk, I’ll describe how Microsoft Research has developed and applied logic engines, such as Z3, and new languages, such as Ivy and F*, to the specification, proof and testing of critical subsystems of Microsoft Azure. F*, Ivy, and Z3 are all open source technologies.

Bio

Thomas (Tom) Ball is a principal researcher and manager at Microsoft Research. In 1999, 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 the Microsoft MakeCode platform for programming with physical computers (www.makecode.com).