Andrea Lattuada

Andrea Lattuada

(click to reveal)@mpi-sws.org

I will be joining the Max Planck Institute for Software Systems (MPI-SWS) as a Research Group Leader in September 2024.

Derek Dreyer and I have open positions for PhD Students and Postdocs who are interested in working on a number of topics in Systems Software Verification, in particular focusing on making verification more practical and usable by engineers and on leveraging advanced reasoning techniques. See my research profile below for more details on my work, and feel free to get in touch.

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.

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 co-started (with Chris Hawblitzel, MSR) 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 am starting to explore the relationship between Rust's Ownership Logic, leveraged by Verus, and separation logic, in particular in the context of the Iris Concurrent Separation Logic Framework: I am interested in exploring ways to bring SMT-style automation to Iris-style proofs, and to bring advanced CSL-based reasoning to SMT-based tools like 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.

🏆 Awards

Journal Publications

Peer-reviewed Publications

Peer-review Service

Workshop talks

  • 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