Vector Clocks in Coq: An Experience Report
arXiv:1406.4291v11 citations
Originality Synthesis-oriented
AI Analysis
This work addresses implementation hurdles for formal methods in real-world distributed systems, but it is incremental as it builds on existing Coq and Dynamo/Riak frameworks.
The authors tackled the challenge of integrating Coq-verified vector clocks into a production Erlang system (Riak), focusing on practical extraction and deployment issues rather than verification.
This report documents the process of implementing vector clocks in the Coq proof assistant for extraction and use in the distributed Dynamo-inspired data store, Riak. In this report, we focus on the technical challenges of using Core Erlang code extracted from the proof assistant in a production-grade Erlang application, as opposed to verification of the model itself.