Words
Andrea Lattuada

Andrea Lattuada

I am a Researcher in the VMware Research Group.

I got my PhD in the Systems Group at ETH Zürich, advised by Prof. Timothy Roscoe.

Here is my CV.

I am interested in systems software verification as a way to substantially improve their safety and reliability, but to achieve this, the verification effort must be commensurate to the value it provides. I have been building verified systems, and extending the available tooling to find and fix inefficiencies. Based on this experience, I started and I 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.

We are writing and verifying complex, concurrent systems programs in Verus. Researchers at the University of Utah are using Verus to write and verify a full-featured microkernel, and Microsoft is writing and verifying durable logs on persistent memory with Verus.

I have worked on techniques for efficient re-scaling and fault-tolerance for streaming data processing system, and I am working on a new dataflow-inspired programming model for Serverless platforms as part of a collaboration with ETH Zurich.

With colleagues at VMware Research and ETH Zurich I am exploring how to specify and verify an Operating System with the goal of providing a useful, verified interface to the client applications rather than just focusing on isolation and security properties.

Peer-reviewed Publications

Peer-review Service

Workshop talks

  • 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