Victor Gomes

OK Google, where is my profile picture?

Research Associate, University of Cambridge.

I am currently working on the Cerberus project (REMS) with Prof. Peter Sewell.
University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD


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.


Recent events I have participated (or will).






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


Project supervisions