Modeling Smart Contracts with Probabilistic Logic Programming

Smart contracts are computer programs that run in a distributed network, the blockchain. These contracts are used to regulate the interaction among parties in a fully decentralized way without the need of a trusted authority and, once deployed, are immutable. The immutability property requires that the programs should be deeply analyzed and tested, in order to ensure that they behave as expected and to avoid bugs and errors. In this paper, we present a method to translate smart contracts into probabilistic logic programs that can be used to analyse expected values of several smart contract’s utility parameters and to get a quantitative idea on how smart contracts variables changes over time. Finally, we applied this method to study three real smart contracts deployed on the Ethereum blockchain.