Formal verification of Ethereum smart contracts using Isabelle/HOL
DOI10.1007/978-3-030-62077-6_7zbMATH Open1476.68156OpenAlexW3097390987MaRDI QIDQ2037985FDOQ2037985
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
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
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)
Cited In (7)
- EthVer: formal verification of randomized Ethereum smart contracts
- Compositional verification of smart contracts through communication abstraction
- The eye of Horus: spotting and analyzing attacks on ethereum smart contracts
- Formal verification of atomicity requirements for smart contracts
- Formal analysis of composable DeFi protocols
- Validation of decentralised smart contracts through game theory and formal methods
- SSCalc: a calculus for Solidity smart contracts
Uses Software
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)
