The Business of Proof

Abstract: With only a few niche exceptions, the software industry had not previously figured out how to make deep use of formal mechanical reasoning based on mathematical logic. At Amazon we have recently seen tremendous adoption of the approach by product groups, with a variety of customer-facing launches that use automated reasoning, and numerous internal proof projects. This talk describes those projects, and tries explain what went well at Amazon. The talk also describes challenges that we face to scale the approach to the next level.

Bio: Dr. Byron Cook, FREng is Professor of Computer Science at University College London (UCL). Byron is also Vice President and Distinguished Scientist at Amazon. Byron’s has worked in a variety of areas over the years, including computer/network security, program analysis/verification, programming languages, theorem proving, hardware design, operating systems, and biological systems.