University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > The business of proof

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

The business of proof

Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

With only a few niche applications, the software industry had not previously figured out how to make deep use of formal mechanical reasoning based on mathematical logic. At Amazon we’ve 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 describes those projects, and captures aspects of why Amazon has been successful where others have been less so.  The talk also describes challenges that we face to scale the approach to the next level. 

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

PPSIS Committee Room (Free School Lane) Faculty of Education, Mary Allan Building,Boulind 8 & 9, Homerton College, Hills Road, Cambridge CB2 8PQ Latimer Room (Old Court), Clare College, Trinity Lane

Other talks

Disentangling preventative & ejective AGN feedback on a population basis with simulations, observations & machine learning Title to be confirmed Optimal metric and approximation of free boundary minimal surfaces Task performance predicts the substitution of feedforward by feedback drive in visual cortex Group Work Title to be confirmed
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity