Formal verification of Ethereum smart contracts using Isabelle/HOL

DOI10.1007/978-3-030-62077-6_7MaRDI QIDQ2037985zbMATHOpenAlexFDO

Authors Maria Ribeiro, P. Adão, Paulo Mateus

Publication date 8 July 2021

Full work available at URL https://doi.org/10.1007/978-3-030-62077-6_7

zbMATH Keywords

Hoare logicformal verificationIsabelle/HOLsolidityEthereumsmart contracts

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Contract theory (moral hazard, adverse selection) (91B41)

Recommendations

• Formal verification of atomicity requirements for smart contracts
• Verification-Led Smart Contracts
• EthVer: formal verification of randomized Ethereum smart contracts
• Compositional verification of smart contracts through communication abstraction
• Validation of decentralised smart contracts through game theory and formal methods

Cited in

(7)

• Formal analysis of composable DeFi protocols
• Formal verification of atomicity requirements for smart contracts
• EthVer: formal verification of randomized Ethereum smart contracts
• SSCalc: a calculus for Solidity smart contracts
• Validation of decentralised smart contracts through game theory and formal methods
• Compositional verification of smart contracts through communication abstraction
• The eye of Horus: spotting and analyzing attacks on ethereum smart contracts

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Formal verification of Ethereum smart contracts using Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2037985)