Andrea Lattuada
andrea@lattuada.me
(click to reveal)@mpi-sws.org
I am a Research Group Leader at the Max Planck Institute for Software Systems (MPI-SWS). I joined in September 2024.
Derek Dreyer and I have open positions for PhD Students and Postdocs who are interested in working on Systems Software Verification, in particular focusing on making verification more practical and usable by engineers and on devising and 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 build verified systems, and extend the available tooling to find and fix inefficiencies.
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 systems, 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.
Advising and Mentoring
Over the last few years I have advised and mentored many brilliant students working with me on a variety of research projects.
With the exception of currently ongoing collaborations, students at ETH Zurich were co-supervised by my advisor, Prof. Timothy Roscoe.
-
Since April 2024 Johanna Polzin, ETH Zurich, Switzerland Bachelor Thesis (in progress)
Co-supervised by Matthias Brun and Prof. David Basin. Johanna is working on modeling a concurrent OS and verifying that it corresponds to a process-centric contract of OS behavior, which can be used as a foundation
for verified applications.
-
August-November 2024 Pranav Srinivasan, VMware Research, US Research Intern
Co-supervised by Jon Howell and Oded Padon. Pranav worked on better understanding the verification performance implications of quantifier instantiation across program modules: this work was presented at the Dafny 2024 Workshop as "Domesticating Automation". Pranav also worked on supporting a decidable logic fragment in Verus which enables a complete and fast decision procedure in the solver.
-
Since 2023 Matthias Brun, ETH Zurich, Switzerland PhD Student (continued collaboration)
Co-supervised by Prof. David Basin. Matthias is working on verifying the
correctness of an operating system's memory management subsystem (page table)
in relation to the memory management hardware (MMU, TLBs), and against a
process-centric contract of OS behavior, which can be used as a foundation
for verified applications.
-
April - October 2022 Matthias Brun, ETH Zurich, Switzerland Master Thesis
📄
Verified Paging for x86-64 in Rust. Part of this work was published as part of "Beyond isolation: OS verification as a foundation for correct applications" at HotOS 2023. Matthias' contributions to Verus were published as part of "Verus: Verifying Rust Programs using Linear Ghost Types" at OOPSLA 2023.
-
Summer 2022 Isitha Subasinghe, ETH Zurich, Switzerland Research Assistant
Isitha contributed support for reasoning about character strings in Verus. This work was published as part of "Verus: Verifying Rust Programs using Linear Ghost Types" at OOPSLA 2023.
-
November 2019 - May 2020 Sára Decova, ETH Zurich, Switzerland Master Thesis
-
November 2019 - May 2020 Matthias Brun, ETH Zurich, Switzerland Research Assistant
Co-supervised by Dmitriy Traytel. Matthias worked on the modeling and verification of the Timely Dataflow's control plane protocol. This work was published as part of "Verified Progress Tracking for Timely Dataflow" at ITP 2021.
-
October 2019 - April 2020 Lorenzo Selvatici, ETH Zurich, Switzerland Master Thesis
-
October 2018 - April 2019 Lorenzo Martini, ETH Zurich, Switzerland Master Thesis
-
July - Aug. 2018 Nazerke Seidan, Eötvös Lorand University, Hungary ETH Summer Student Research Fellowship
Co-supervised by Frank McSherry. Visualizing progress tracking, the control plane messages, of Timely Dataflow, a distributed dataflow data-processing engine.