SSCalc: a calculus for Solidity smart contracts

DOI10.1007/978-3-031-47115-5_11MaRDI QIDQ6550597zbMATH OpenFDO

Authors Diego Marmsoler, Billy Thornton

Publication date 5 June 2024

Full work available at URL https://doi.org/10.1007/978-3-031-47115-5_11

zbMATH Keywords

Isabelleprogram verificationsmart contractsSolidity

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Formal verification of Ethereum smart contracts using Isabelle/HOL
• Formal verification of atomicity requirements for smart contracts
• Is Solidity Solid Enough?
• Compositional verification of smart contracts through communication abstraction
• Verification-Led Smart Contracts

Cites work

• An Isabelle proof method language
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 1424012 (Why is no real title available?)
• Is Solidity Solid Enough?
• Isabelle/HOL. A proof assistant for higher-order logic
• Secure Microkernels, State Monads and Scalable Refinement
• Verification of sequential and concurrent programs

Cited in

(1)

• Translation certification for smart contracts

This page was built for publication: SSCalc: a calculus for Solidity smart contracts

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