Invariant Safety for Distributed Applications

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.
Complete list of metadatas

https://hal.inria.fr/hal-02052012
Contributor : Marc Shapiro <>
Submitted on : Wednesday, March 6, 2019 - 7:46:42 PM
Last modification on : Friday, July 5, 2019 - 3:26:03 PM
Long-term archiving on : Friday, June 7, 2019 - 5:34:26 PM

Files

authorversion-soteria.pdf
Files produced by the author(s)

Licence


Copyright

Identifiers

  • HAL Id : hal-02052012, version 1
  • ARXIV : 1903.02759

Citation

Sreeja Nair, Gustavo Petri, Marc Shapiro. Invariant Safety for Distributed Applications. Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), Mar 2019, Dresden, Germany. ⟨hal-02052012⟩

Share

Metrics

Record views

56

Files downloads

73