Research Associate, University of Cambridge.

I am currently working on the Cerberus project (REMS) with Prof. Peter Sewell.

Research

My research interests include theorem-proving, formal verification, system programming, compilers, semantics of programming languages, Kleene algebras, separation logic, distributed and concurrent systems. Here are some of the projects I work on:

Cerberus: A de facto and formal semantic model for the C programming language. Cerberus is an executable semantics, serving as a test oracle and allowing programmers to explore the range of behaviours of a C program. As opposed to ISO C, this is finally a step to a clear, unambiguous and mechanised semantics for C. This project is a collaboration with Prof. Peter Sewell and Kayvan Memarian. The Cerberus web interface lets one interactively, randomly or exhaustively explore the behaviour of small C tests programs. You can find more information about the project at the Cerberus webpage.

Formal verification of CRDTs. In this project, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms.

Algebraic approach for program verification: During my PhD, I explored an algebraic approach to the development of construction and verification tools. Computational algebras, such as Kleene Algebras with tests, are used to give an algebraic semantics to programs and suffice to express its control flow. The whole development is done within the proof-assistant Isabelle/HOL and it is itself correct by construction. The approach has been successfully applied to simple imperative while-programs, where Hoare logic was derived from the algebra; to while-programs with pointers, in which a simple implementation of separation logic based on power series and quantales is used; and to concurrent programs, where a variant of concurrent Kleene algebra is used to derive the inference rules of the rely-guarantee method.

Publications

My publications are also available on DBLP and Google Scholar.

Events

Recent events I have participated (or will).

2019

• POPL 2019

2018

• S-REPLS
• ISO WG14
• LLVM Euro Dev Meeting 2018
• ARW 2018

2017

• APLAS 2017
• OOPSLA 2017
• POPL 2017
• FreeBSD DevSummit 2017

Past

• FM 2016
• Kent Concurrency Workshop
• MGS

Teaching

As a former bye-fellow of Fitzwilliam College, I taught and supervised a number of students.

Cambridge

Project supervisions

• Cristina Matache, Part II Cambridge Computer Science Tripos project supervision. Project title: Formalisation of the lambda-mu-T calculus in Isabelle/HOL.
• Michael Rawson, Part II Cambridge Computer Science Tripos project supervision with Dominic Mulligan. Project title: Verified metatheory and type checking for the simply-typed lambda calculus.

Lectures

• Logic and Proofs, covering for Prof. Larry Paulson (2017 - 2018)

Supervisions

• Semantics of Programming Languages (2016 - 2019)
• Discrete Mathematics (2016 - 2018)
• Concepts in Programming Languages (2016 - 2018)

Sheffield

Demonstrations

• Foundations of Computer Science (2013 - 2015)
• Automata, Logic and Computation (2014 - 2015)
• Software Hut (2014 - 2015)
• Software and Hardware Verification (2013 - 2015)