I am developing Verus: a semi-automatic verification tool for the Rust programming language. I am part of a collaborative effort to dramatically lower the costs associated with verifying software systems with the goal of improving the reliability and security of new systems software.

I also have been working on techniques for re-scaling and fault-tolerance for streaming data processing system, with a strong focus on efficiency.

Publications

• Conference Paper, October 2023
  Verus: Verifying Rust Programs using Linear Ghost Types, Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel

  Proceedings of the ACM on Programming Languages (OOPSLA'23)
• [to appear] Conference Paper, 2023
  Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems, Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno

  17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23)
• Conference Paper, 2022 - Distinguished Paper Award
  Linear Types for Large-Scale Systems Verification, Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel

  Proceedings of the ACM on Programming Languages (OOPSLA'22)
• Conference Paper, June 2021
  Verified Progress Tracking for Timely Dataflow [Technical Report], Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel
  Interactive Theorem Proving (ITP'21)
• Conference Paper, November 2020
  Storage Systems are Distributed Systems (So Verify Them That Way!), Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno
  14th USENIX Symposium on Operating Systems Design and Implementation (OSDI'20)
• Conference Paper, September 2020
  Shared Arrangements: practical inter-query sharing for streaming dataflows [Technical report] [Talk video], Frank McSherry, Andrea Lattuada, Malte Schwarzkopf, Timothy Roscoe
  Proceedings of the VLDB Endowment, Volume 13, No. 10 (VLDB 2020)
• Conference Paper, August 2019
  Megaphone: Latency-conscious state migration for distributed streaming dataflows, Moritz Hoffmann, Andrea Lattuada, Frank McSherry, Vasiliki Kalavri, John Liagouris, Timothy Roscoe
  Proceedings of the VLDB Endowment, Volume 12, 2018-2019 (VLDB 2019)
• Workshop Paper, June 2018
  Latency-conscious dataflow reconfiguration, Moritz Hoffmann, Frank McSherry, Andrea Lattuada
  Proceedings of the 5th ACM SIGMOD Workshop on Algorithms and Systems for MapReduce and Beyond (BeyondMR'18)
• Conference Paper, April 2018
  SnailTrail: Generalizing critical paths for online analysis of distributed dataflows [Technical report], Moritz Hoffmann, Andrea Lattuada, John Liagouris, Vasiliki Kalavri, Desislava Dimitrova, Sebastian Wicki, Zaheer Chothia, Timothy Roscoe
  Proceedings of the 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI'18)
• Workshop Paper, June 2016
  Faucet: a user-level, modular technique for flow control in dataflow engines, Andrea Lattuada, Frank McSherry, Zaheer Chotia
  Proceedings of the 3rd ACM SIGMOD Workshop on Algorithms and Systems for MapReduce and Beyond (BeyondMR'16)

• October 2017
  [Poster] No-sync: coordination-free fault-tolerance in streaming, Andrea Lattuada, Vasiliki Kalavri, Moritz Hoffmann, Frank McSherry
  SOSP'17 - Poster session
• April 2017
  [Poster] Differential durability: fault-tolerant distributed differential computation, Andrea Lattuada, Vasiliki Kalavri, Moritz Hoffman, Frank McSherry
  Eurosys'17 - Poster session
• April 2017
  [Poster] SnailTrail: Online Bottleneck Detection for your Dataflow, R. Sager, John Liagouris, Desislava Dimitrova, Andrea Lattuada, Vasiliki Kalavri, Zaheer Chothia, Moritz Hoffmann, Timothy Roscoe
  Eurosys'17 - Poster session

Peer-review service

• 2021
  ASPLOS '22 − External Review Committee
• 2021
  OSDI '21 − Artifact Evaluation Committee
• 2018
  VLDB Journal − Reviewer