Skip to Main content Skip to Navigation
New interface
Conference papers

Formal verification of smart contracts based on users and blockchain behaviors models

Abstract : Blockchain technology has attracted increasing attention in recent years. One reason for this new trend is the introduction of on-chain smart contracts enabling the implementation of decentralized applications in trust-less environments. Along with its adoption, attacks exploiting smart contract vul-nerabilities are inevitably growing. To counter these attacks and avoid breaches, several approaches have been explored such as documenting vulnerabilities or model checking using formal verification. However, these approaches fail to capture the blockchain and users behavior properties. In this paper, we propose a novel formal modeling approach to verify a smart contract behavior in its execution environment. We apply this formalism on a concrete smart contract example and analyze its breaches with a statistical model checking approach.
Document type :
Conference papers
Complete list of metadata
Contributor : Elyes Ben Hamida Connect in order to contact the contributor
Submitted on : Friday, April 6, 2018 - 4:32:14 PM
Last modification on : Tuesday, October 18, 2022 - 8:34:05 AM


Files produced by the author(s)


  • HAL Id : hal-01760787, version 1



Tesnim Abdellatif, Kei-Léo Brousmiche. Formal verification of smart contracts based on users and blockchain behaviors models. IFIP NTMS International Workshop on Blockchains and Smart Contracts (BSC), Feb 2018, Paris, France. ⟨hal-01760787⟩



Record views


Files downloads