Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there is no logic-based model for blockchains available. We introduce BCL, a dynamic logic to reason about blockchain updates, and show that BCL is sound and complete with respect to a simple blockchain model.
@article{arxiv.1707.01766,
title = {A Logic of Blockchain Updates},
author = {Kai Brünnler and Dandolo Flumini and Thomas Studer},
journal= {arXiv preprint arXiv:1707.01766},
year = {2017}
}