Formally verifying the properties of a distributed file system, with Availability under Partition properties. The file system consists of interdependent CRDT objects under a strong safety invariant (tree shape). Paper by Mahsa Najafzadeh, Marc Shapiro and Patrick Eugster, published at VMCAI 2018. The paper is available here.
Jan 30
VMCAI 2018: “Co-Design and Verification of an Available File System”
