Showing cs.LOShow all
2 papers · 1 filter
cs.LO2023
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
Franck Cassez, Joanne Fuller, Milad K. Ghale +2
The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed…
cs.LO2022
Deductive Verification of Smart Contracts with Dafny
Franck Cassez, Joanne Fuller, Horacio Mijail Anton Quiles
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our…