@inproceedings{6f5a41c6c0894fcf8c562c8cf80ecb4a,
title = "Verifying eventual consistency of optimistic replication systems",
abstract = "We address the verification problem of eventual consistency of optimistic replication systems. Such systems are typically used to implement distributed data structures over large scale networks. We introduce a formal definition of eventual consistency that applies to a wide class of existing implementations, including the ones using speculative executions. Then, we reduce the problem of checking eventual consistency to reachability and model checking problems. This reduction enables the use of existing verification tools for message-passing programs in the context of verifying optimistic replication systems. Furthermore, we derive from these reductions decision procedures for checking eventual consistency of systems implemented as finite-state programs communicating through unbounded unordered channels.",
keywords = "message passing concurrency, model checking, static program analysis",
author = "Ahmed Bouajjani and Constantin Enea and Jad Hamza",
year = "2014",
month = feb,
day = "11",
doi = "10.1145/2535838.2535877",
language = "English",
isbn = "9781450325448",
series = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
pages = "285--296",
booktitle = "POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
note = "41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 ; Conference date: 22-01-2014 Through 24-01-2014",
}