I’ve spent the last couple of years working at Google Research. For the first 5–6 months, I was working in London in an office nestled between King’s Cross station and the iconic St Pancras station. This location was ideal for me because I was still living in Cambridge at the time and it was a very easy journey to either of these stations from Cambridge.

I started off working on privacy and security in operating systems. This led to fun experiments with UW’s impressive Serval that automatically verifies machine code and Bart Jacobs’ amazing VeriFast tool whose user interface transformed my thinking about auto-active verification.

After that, I lead the Rust verification project at Google: a project focused on usability of formal verification. I wrote surveys of the available Rust verification tools in 2020 and 2021; I used a risk based approach to research planning; I collaborated with some usability researchers on a paper about “making formal normal”; and I used KLEE to understand some of the infrastructure barriers to using verification tools on real Rust code. For example, I found and filled gaps in language feature support, library support, runtime/linker support, etc. (See the workshop presentation for details [pdf] [video].) With these extensions in hand, I was able to try to run verification tools on large, complex, real-world Rust code such as “Rust for Linux” [pdf] and the Rust rewrite of CoreUtils to understand the remaining issues.

For the last 2–3 months, I have been working on a hardware-software codesign project. These are always a lot of fun because you start with a huge design space and then gradually narrow down what parts of the task are best solved by the programmer, the compiler, the runtime and libraries, or the hardware. A critical part of these projects is about enabling and encouraging the right kind of collaboration between subteams with radically different expertise: hardware, software, tools, systems, etc. So I built a performance modeling tool to enable software and hardware engineers to find the right design compromise: discovering the performance bottlenecks in the code and exploring different microarchitecture and vectorization choices to overcome them.

I’ve learned a lot of new things over the last two years but I’ve decided that it is time to move on. So, today I bid my colleagues farewell and leave Google Research.