A logic of blockchain updates
Kai Brünnler, Dandolo Flumini, Thomas Studer · Journal of Logic and Computation · 2020
Abstract 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 are only few logic-based models for blockchains available. We introduce $\mathsf{BCL}$, a dynamic logic to reason about blockchain updates, and show that $\mathsf{BCL}$ is sound and complete with respect to a simple blockchain model.