Andrea Lattuada
andrea@lattuada.me
(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.