2019/03/07 by Sreeja Nair, Nair, Sreeja, Gustavo Petri +3
Computer Science · #Databases (cs.DB) #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Parallel #Security and Verification in Computing #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1903.02759
openalex publication_date 2019/03/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We study a proof methodology for verifying the safety of data invariants of highly-available distributed applications that replicate state. The proof is (1) modular: one can reason about each individual operation separately, and (2) sequential: one can reason about a distributed application as if it were sequential. We automate the methodology and illustrate the use of the tool with a representative example.