13 citations · 35 across the 16 of their papers we have counts for
5 papers · 1 filter
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…
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…
Verification of the Incremental Merkle Tree Algorithm with Dafny
Franck Cassez
The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental M…
Control and Synthesis of Non-Interferent Timed Systems
Gilles Benattar, Franck Cassez, Didier Lime +1
In this paper, we focus on the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference prop…
A Note on Fault Diagnosis Algorithms
Franck Cassez
In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to t…