ABSTRACT

In three teams at AWS, software developers now use model checking to demonstrate some level of memory safety of the code they write.  More than 20 developers have written more than 800 memory safety proofs of entry points in more than 18 projects.  The proofs are part of the code review process, and are checked against every proposed code change, resulting in as many as 6000 proofs being checked in continuous integration every day.  In this talk, I describe some of the things we have done to make bounded model checking just another form of unit test at AWS.