How Amazon web services uses formal methods
- 23 March 2015
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 58 (4), 66-73
- https://doi.org/10.1145/2699417
Abstract
Engineers use TLA+ to prevent serious but subtle bugs from reaching production.Keywords
This publication has 11 references indexed in Scilit:
- Why Amazon Chose TLA +Lecture Notes in Computer Science, 2014
- Using lightweight modeling to understand chordACM SIGCOMM Computer Communication Review, 2012
- Towards Verification of the Pastry Protocol Using TLA +Lecture Notes in Computer Science, 2011
- The Farsite projectACM SIGOPS Operating Systems Review, 2007
- Assessing the Relationship between Software Assertions and Faults: An Empirical Investigation2006 17th International Symposium on Software Reliability Engineering, 2006
- Fast PaxosDistributed Computing, 2006
- Checking a Multithreaded Algorithm with + CALLecture Notes in Computer Science, 2006
- Checking Cache-Coherence Protocols with TLA+Formal Methods in System Design, 2003
- High-Level Specifications: Lessons from IndustryLecture Notes in Computer Science, 2003
- Specifying and verifying fault-tolerant systemsLecture Notes in Computer Science, 1994