Distinguished Lecture: Automated Formal Reasoning About AWS Systems

Speaker: Byron Cook , Amazon
UCL Contact: Julia Savage (Visitors from outside UCL please email in advance).
Date/Time: 08 Dec 16, 15:00 - 16:30
Venue: 4.05, 66-72 Gower Street
Further Information:

A drinks reception will follow in the common room on Ground Floor in 66-72 Gower Street.

Abstract

Automatic and semiautomatic mechanical theorem provers are now being used within Amazon AWS to find proofs in mathematical logic that establish desired properties of key AWS components. In this session, we outline these efforts and discuss how mechanical theorem provers are used to replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system.

Byron Cook

Byron Cook is a Professor at UCL and a Senior Principal at Amazon Web Services.