相关论文: Declarative Smart Contracts

Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an…

Smart contracts are computer programs running on blockchains to implement Decentralized Applications. The absence of contract specifications hinders routine tasks, such as contract understanding and testing. In this work, we propose a…

We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications,…

We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination…

Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development,…

Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens…

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…

Formal verification entails testing software to ensure it operates as specified. Smart contracts are self-executing contracts with the terms of the agreement directly written into lines of code. They run on blockchain platforms and…

Decentralized Finance (DeFi) is a system of financial products and services built and delivered through smart contracts on various blockchains. In the past year, DeFi has gained popularity and market capitalization. However, it has also…

A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain,…

Smart contracts codify real-world transactions and automatically execute the terms of the contract when predefined conditions are met. This paper proposes SmartML, a modeling language for smart contracts that is platform independent and…

We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value…

Smart contracts are programs that execute transactions involving independent parties and cryptocurrencies. As programs, smart contracts are susceptible to a wide range of errors and vulnerabilities. Such vulnerabilities can result in…

Smart contracts are the building blocks of the "code is law" paradigm: the smart contract's code indisputably describes how its assets are to be managed - once it is created, its code is typically immutable. Faulty smart contracts present…

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…

Blockchains are being positioned as the "technology of trust" that can be used to mediate transactions between non-trusting parties without the need for a central authority. They support transaction types that are native to the blockchain…

Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program…

Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are…

Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and…

More than eight million smart contracts have been deployed into Ethereum, which is the most popular blockchain that supports smart contract. However, less than 1% of deployed smart contracts are open-source, and it is difficult for users to…