How Amazon web services uses formal methods

2015/03/23 by Chris Newcombe, Tim Rath, Fan Zhang +3 · 4 citations
Computer Science · #Distributed systems and fault tolerance #Advanced Malware Detection Techniques #Software System Performance and Reliability

paper · doi:10.1145/2699417

openalex publication_date 2015/03/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/25

Abstract

Engineers use TLA+ to prevent serious but subtle bugs from reaching production.

Citations

• Using lightweight modeling to understand chord

Cited by

• Reasoning about identifier spaces: How to make Chord correct
• Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
• On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
• Pamela Zave [wikipedia]

Related

• To Err is AI : A Case Study Informing LLM Flaw Reporting Practices
• LLMs in Coding and their Impact on the Commercial Software Engineering Landscape
• The TLA+ Toolbox
• ADA PROWAG Status and Common Issues/Solutions
• Comparative Analysis of the Code Generated by Popular Large Language Models (LLMs) for MISRA C++ Compliance