I am a computer scientist with interest in formal methods, more specifically automated verification techniques such as software verification and model-checking, static analysis. I have a strong expertise in modelling and verification of concurrent (distributed) systems as well as static analysis and deductive verification.

I have contributed several important results in the theoretical foundations of verification of concurrent systems and also developed software analysis tools (static analysis, model-checking), Scala packages (SMT-solvers, finite automata). More recently I started to apply formal verification techniques to blockchain components with the verification-friendly language Dafny.

Experience

I am currently heading the research effort at Mantle, an Ethereum rollup. My interest for blockchain technology started in 2019 when I joined ConsenSys and worked on several research projects including the verification of the Beacon Chain, verification of the Deposit Contract, formal verification of Smart Contracts in Dafny, and a semantics of the EVM in Dafny.

Here are some recent projects I am involved in:

• formal verification of smart contracts, An EVM in Dafny

• formal specification and verification of the Eth2.0 Phase 0 specification (Beacon chain). We use the verification-aware programming language Dafny to formally (i.e. rigorously and mathematically) verify the Eth2 specification.

• formal verification of the Deposit Smart Contract algorithms. I have developed the first fully mechanised correctness proof of the incremental Merkle tree algorithm in Dafny.

Before joining ConsenSys, I worked as a research scientist/academic for 25 years, at the French National Centre for Scientific Research (CNRS, France), National ICT Australia (NICTA now DATA61, Sydney AU) and Macquarie University (Sydney AU).

Awards

• Test-of-Time Award, CONCUR’22, The Impressive Power of Stopwatches
• Marie Curie Fellow 2008–2011, Marie Curie Fellowship, individual EU research excellence competitive research grant.
• Best Paper awards:
  • LPAR’15, Verification of Concurrent Programs Using Trace Abstraction Refinement,
  • FMICS’22 Deductive Verification of Smart Contracts with Dafny

Professional Memberships

I have been an ACM member since 2008, and was an IEEE Member from 2009 to 2014. I am a Marie Curie Fellow, was awarded a Marie Curie Fellowship (an individual EU research excellence competitive research grant) in 2008–2011.

Publications

I have published more than 80 research papers (DBLP entries) in peer-reviewed journals & conferences, 1 US patent and several software packages. I serve regularly on program committees of top-tier conferences.