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.
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 was involved in are:
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).
- 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
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.
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.