Andrea Lattuada
andrea@lattuada.me
I lead the Principled Systems Group at the Max Planck Institute for Software Systems (MPI-SWS). I joined in September 2024.
Between the beginning of 2023 and the first half of 2024 I was a Researcher in the VMware Research Group. I got my PhD at the end of 2022 in the Systems Group at ETH Zürich, advised by Prof. Timothy Roscoe.
At the moment I do not have openings for internships, student applications, HiWi (UdS) or RIL projects.
I am a researcher and software engineer with experience in systems, databases, formal methods, and formal verification.
You can find my academic profile at
/research.
I co-started and co-lead the Verus project, Verus is a tool to rapidly verify the correctness of systems code written in Rust.
The Verus project involves members from VMware Research, Microsoft Research, Carnegie Mellon University, ETH Zurich, University of Washington, University of Michigan, University of Wisconsin-Madison, and others.
There are a number of research and industry projects using and developing Verus.
The design and implementation of a lock-free ring-buffer with contiguous reservations
03 June 2019
This is the story of how
James Munns and I designed and implemented (two versions!) of an high-perf lock-free ring-buffer for cross-thread communication. If any of those words look scary to you, don't fret, we'll explain everything from the basics.
A hammer you can only hold by the handle
05 November 2018
Today we're looking at the rust borrow checker from a different perspective. As you may know, the borrow checker is designed to safely handle memory allocation and ownership, preventing accessess to invalid memory and ensuring data-race freedom. This is a form of resource management: the borrow checker is tracking who's in charge of a chunk of memory, and who is currently allowed to read or write to it. In this post, we'll see how these facilities can be used to enforce higher-level API constraints in your libraries and software. Once you're familiar with these techniques, we'll cover how the same principles apply to advanced memory management and handling of other more abstract resources.
Continue reading