Vector Clocks in Coq: An Experience Report
Distributed, Parallel, and Cluster Computing
2014-06-18 v1 Programming Languages
Software Engineering
Abstract
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.
Cite
@article{arxiv.1406.4291,
title = {Vector Clocks in Coq: An Experience Report},
author = {Christopher Meiklejohn},
journal= {arXiv preprint arXiv:1406.4291},
year = {2014}
}