Use of Formal Methods at Amazon Web Services

The following article describing the use of TLA+ at Amazon appeared in the April, 2015 issue of CACM:

    How Amazon Web Services Uses Formal Methods
    Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff
    Communications of the ACM, Vol. 58 No. 4, Pages 66-73
    available on-line

Also available is an earlier version of the article.

The following paper appeared in the ABZ 2014 conference:

    Why Amazon Chose TLA+
    Chris Newcombe
    Abstract State Machines, Alloy, B, TLA, VDM, and Z
    Lecture Notes in Computer Science Volume 8477, 2014, pp 25-39
    available from the publisher