Faucet: a user-level, modular technique for flow control in dataflow engines. - Andrea Lattuada 001; Frank McSherry; Zaheer Chothia (BeyondMR@SIGMOD, 2016)

SnailTrail: Generalizing Critical Paths for Online Analysis of Distributed Dataflows. - Moritz Hoffmann 001; Andrea Lattuada 001; John Liagouris; Vasiliki Kalavri; Desislava C. Dimitrova; Sebastian Wicki; Zaheer Chothia; Timothy Roscoe (NSDI, 2018)

Latency-conscious dataflow reconfiguration. - Moritz Hoffmann 001; Frank McSherry; Andrea Lattuada 001 (BeyondMR@SIGMOD, 2018)

Megaphone: Live state migration for distributed streaming dataflows. - Moritz Hoffmann 001; Andrea Lattuada 001; Frank McSherry; Vasiliki Kalavri; John Liagouris; Timothy Roscoe (CoRR, 2018)

K-Pg: Shared State in Differential Dataflows. - Frank McSherry; Andrea Lattuada 001; Malte Schwarzkopf (CoRR, 2018)

Megaphone: Latency-conscious state migration for distributed streaming dataflows. - Moritz Hoffmann 001; Andrea Lattuada 001; Frank McSherry; Vasiliki Kalavri; John Liagouris; Timothy Roscoe (Proc. VLDB Endow., 2019)

Storage Systems are Distributed Systems (So Verify Them That Way!). - Travis Hance; Andrea Lattuada 001; Chris Hawblitzel; Jon Howell; Rob Johnson 001; Bryan Parno (OSDI, 2020)

Shared Arrangements: practical inter-query sharing for streaming dataflows. - Frank McSherry; Andrea Lattuada 001; Malte Schwarzkopf; Timothy Roscoe (Proc. VLDB Endow., 2020)

Verified Progress Tracking for Timely Dataflow. - Matthias Brun 002; Sára Decova; Andrea Lattuada 001; Dmitriy Traytel (ITP, 2021)

Formalization of Timely Dataflow's Progress Tracking Protocol. - Matthias Brun 002; Sára Decova; Andrea Lattuada 001; Dmitriy Traytel (Arch. Formal Proofs, 2021)

Timestamp tokens: a better coordination primitive for data-processing systems. - Andrea Lattuada 001; Frank McSherry (CoRR, 2022)

Linear types for large-scale systems verification. - Jialin Li 001; Andrea Lattuada 001; Yi Zhou 025; Jonathan Cameron; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2022)

You may not need synchronization (in streaming systems). - Andrea Lattuada 001 (2022)

Beyond isolation: OS verification as a foundation for correct applications. - Matthias Brun 002; Reto Achermann; Tej Chajed; Jon Howell; Gerd Zellweger; Andrea Lattuada 001 (HotOS, 2023)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

Anvil: Verifying Liveness of Cluster Management Controllers. - Xudong Sun 013; Wenjie Ma; Jiawei Tyler Gu; Zicheng Ma; Tej Chajed; Jon Howell; Andrea Lattuada 001; Oded Padon; Lalith Suresh 001; Adriana Szekeres; Tianyin Xu (OSDI, 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Unlocking True Elasticity for the Cloud-Native Era with Dandelion. - Tom Kuchler; Pinghe Li; Yazhuo Zhang; Lazar Cvetkovic; Boris Goranov; Tobias Stocker; Leon Thomm; Simone Kalbermatter; Tim Notter; Andrea Lattuada 001; Ana Klimovic (CoRR, 2025)