Invariant Safety for Distributed Applications
Distributed, Parallel, and Cluster Computing
2019-03-08 v1 Databases
Formal Languages and Automata Theory
Abstract
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.
Cite
@article{arxiv.1903.02759,
title = {Invariant Safety for Distributed Applications},
author = {Sreeja Nair and Gustavo Petri and Marc Shapiro},
journal= {arXiv preprint arXiv:1903.02759},
year = {2019}
}
Comments
Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), Mar 2019, Dresden, Germany. https://novasys.di.fct.unl.pt/conferences/papoc19/