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.

About Byron Cook

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

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.