software . 2020

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic - Coq Formalization

Léon Gondelman; Simon Oddershede Gregersen; Abel Nieto; Amin Timany; Lars Birkedal;
Open Source
  • Published: 05 Oct 2020
  • Publisher: Zenodo
Abstract
<p>We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the causally-consistent distributed database in Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems. We demonstrate that our specifications are useful, by proving the correctness of small, but tricky, synthetic examples involving causal dependency and by verifying a session manager library implemented on top of the distri...
Subjects
free text keywords: distributed systems, separation logic, higher-order logic, concurrency, formal verification
Download fromView all 4 versions
Zenodo
Software . 2020
Provider: Datacite
Zenodo
Software . 2020
Provider: Datacite
Zenodo
Software . 2020
Provider: Zenodo
Zenodo
Software . 2020
Provider: Zenodo
Any information missing or wrong?Report an Issue