Research Associate, University of Cambridge.

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

victor.gomes@cl.cam.ac.uk University of CambridgeComputer Laboratory

William Gates Building

15 JJ Thomson Avenue

Cambridge CB3 0FD

# 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.

# Events

Recent events I have participated (or will).

### 2019

### 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)