Words
Andrea Lattuada

Andrea Lattuada

I am soon to start at a new position in industry.

I led the Principled Systems Group at the Max Planck Institute for Software Systems (MPI-SWS) from September 2024 till June 2025.

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.

Verus Logo 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.

🏆 Research Awards

Selected talks

  • Invited talk at AWS Identity, Amazon Inc., Remote (October 2024)
    Verus – Efficient Verification of Rust Programs
  • New England Verification Workshop 2024, MIT CSAIL, Cambridge, Massachusetts, USA
    Tunable automation for SMT-based verification in Verus
  • Dafny 2024 Workshop at POPL 2024, Paris, France
    Co-author of Domesticating Automation

    To be presented by Pranav Srinivasan
  • Rust Verification Workshop (RW2023) at ETAPS 2023, Paris, France
    Rust Ghost Code
  • Invited talk at the New England Verification Workshop 2022, MIT CSAIL, Cambridge, Massachusetts, USA
    Verus -- SMT-based verification of low-level systems code
  • Rust Verification Workshop (RW2022) at ETAPS 2022, Munich / Garching, Germany
    Verus -- SMT-based verification of low-level systems code

Community talks

  • June 2023, Zürich Rust Meetup, ETH Zurich, Switzerland
    Verus -- Verified Rust for low-level systems code
  • Rust Devroom at FOSDEM 2019, Brussels, Belgium
    Containing the RDMA plasma
  • Rustfest 2017, Zürich, Switzerland
    A hammer you can only hold by the handle
  • March 2017, Papers we love, Zürich, Switzerland
    Naiad: A timely dataflow system

Peer-reviewed Publications

Journal Publications

Workshops, Conferences, Peer-review Service

Blog Posts

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.
Continue reading

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