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. 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), and recently Dafny-verified programs.
I currently work at ConsenSys Software R&D as an Applied Researcher, and the main projects I am involved in are:
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).
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.