Related papers: Albert, an intermediate smart-contract language fo…
Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson…
Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Its smart contract language is called Michelson and it has been designed with formal verification in mind. In this article, we present…
Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the…
Tezos is an innovative blockchain that improves on several aspects compared to more established blockchains. It offers an original proof-of-stake consensus algorithm and can be used as a decentralized smart contract platform. It has the…
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource…
A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging…
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically…
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like…
Once you have invented digital money, you may need a ledger to track who owns what -- and an interface to that ledger so that users of your money can transact. On the Tezos blockchain this implies: a smart contract (distributed program),…
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich…
This paper presents TXSC, a framework that provides smart contract developers with transaction primitives. These primitives allow developers to write smart contracts without the need to reason about the anomalies that can arise due to…
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in…
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high…
Blockchain technologies, such as smart contracts, present a unique interface for machine-to-machine communication that provides a secure, append-only record that can be shared without trust and without a central administrator. We study the…
A key component of blockchain technology is the ledger, viz., a database that, unlike standard databases, keeps in memory the complete history of past transactions as in a notarial archive for the benefit of any future test. In…
The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like…
Smart contracts are autonomous software executing predefined conditions. Two of the biggest advantages of the smart contracts are secured protocols and transaction costs reduction. On the Ethereum platform, an open-source blockchain-based…
We present a smart legal contract platform to support a wide range of smart legal contract use cases. We see this as a step towards improving existing approaches to representing the complexity of legal agreements and executing aspects of…
A smart contract is an interactive program that governs funds in the realm of a single cryptocurrency. Yet, the many existing cryptocurrencies have spurred the design of cross-chain applications that require interactions with multiple…
The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults rooted in out-of-order interactions with contract endpoints. We…