Verification-Led Smart Contracts

DOI10.1007/978-3-030-43725-1_9zbMATH Open1520.91440OpenAlexW2954438468MaRDI QIDQ6166532FDOQ6166532

Authors: Richard Banach 

Publication date: 3 August 2023

Published in: Financial Cryptography and Data Security (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-43725-1_9

Recommendations

• Formal verification of atomicity requirements for smart contracts
• Validation of decentralised smart contracts through game theory and formal methods
• Compositional verification of smart contracts through communication abstraction

zbMATH Keywords

verificationrefinementEvent-Bblockchainsmart contractRodinSolidity

Mathematics Subject Classification ID

Cryptography (94A60) Actuarial science and mathematical finance (91G99)

Cites Work

• Lem: reusable engineering of real-world semantics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Refinement Calculus
• Modeling in Event B. System and software engineering.
• The B-Book
• Title not available (Why is that?)
• Superposition refinement of reactive systems
• Atomic actions, and their refinements to isolated protocols
• Title not available (Why is that?)

Cited In (9)

• Smart Contract Execution - the (+-)-Biased Ballot Problem.
• Compositional verification of smart contracts through communication abstraction
• Formal verification of Ethereum smart contracts using Isabelle/HOL
• Formal verification of atomicity requirements for smart contracts
• Soft contract verification
• Validation of decentralised smart contracts through game theory and formal methods
• Adding concurrency to smart contracts
• Smart contract derivatives
• SSCalc: a calculus for Solidity smart contracts

This page was built for publication: Verification-Led Smart Contracts

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