13 citations · 35 across the 16 of their papers we have counts for
17 papers
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…
Formal Verification of the Ethereum 2.0 Beacon Chain
Franck Cassez, Joanne Fuller, Aditya Asgaonkar
We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethere…
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…
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
Franck Cassez, Peter Gjøl Jensen, Kim Guldstrand Larsen
We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discr…
Timed Automata for Modelling Caches and Pipelines
Franck Cassez, Pablo González de Aledo Marugán
In this paper, we focus on modelling the timing aspects of binary programs running on architectures featuring caches and pipelines. The objective is to obtain a timed automaton mod…
The Complexity of Synchronous Notions of Information Flow Security
Franck Cassez, Ron van der Meyden, Chenyi Zhang
The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in wh…
Predictability of Event Occurrences in Timed Systems
Franck Cassez, Alban Grastien
We address the problem of predicting events' occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of…
Proceedings Seventh Conference on Systems Software Verification
Franck Cassez, Ralf Huuck, Gerwin Klein +1
This volume contains the papers accepted at the 7th Systems Software Verification Conference (SSV 2012), held in Sydney, November 28-30, 2012. The aim of SSV workshops and conferen…
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…
Controllers with Minimal Observation Power (Application to Timed Systems)
Peter Bulychev, Franck Cassez, Alexandre David +3
We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The…
Computation of WCET using Program Slicing and Real-Time Model-Checking
Jean-Luc Béchennec, Franck Cassez
Computing accurate WCET on modern complex architectures is a challenging task. This problem has been devoted a lot of attention in the last decade but there are still some open iss…
Dynamic Observers for Fault Diagnosis of Timed Systems
Franck Cassez
In this paper we extend the work on \emph{dynamic ob\-servers} for fault diagnosis to timed automata. We study sensor minimization problems with static observers and then address t…
Timed Games for Computing Worst-Case Execution-Times
Franck Cassez
In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms with caches and pipelines. The methodology we propose consists of 3 steps…
Fault Diagnosis with Dynamic Observers
Franck Cassez, Stavros Tripakis
In this paper, we review some recent results about the use of dynamic observers for fault diagnosis of discrete event systems. Fault diagnosis consists in synthesizing a diagnoser…
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…
The Complexity of Codiagnosability for Discrete Event and Timed Systems
Franck Cassez
In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform c…