Andrea Lattuada will join MPI-SWS as a Research Group Leader in September 2024. Before joining MPI-SWS, Andrea worked as a researcher in the VMware Research Group. He completed his PhD at ETH Zurich, where he focused on systems for distributed data processing and systems software verification.

Andrea builds verification tools and formally verified systems with a focus on pragmatism. He co-started and co-leads the Verus project. Verus is a tool used by various industry and academic projects to rapidly verify the correctness of systems code written in Rust. At MPI, his research group will continue to leverage software verification to substantially improve the safety and reliability of systems software. This will involve developing new and more powerful techniques to reason about complex software, improving the usability and efficiency of verification tools, and devising principled and cost-effective development disciplines for verified software. Andrea also collaborates with researchers at ETH Zürich on new programming models for the cloud, and on building a verified operating system with a compact, well-specified programming interface.

Andrea’s group has open positions for doctoral students, postdocs, and interns who are interested in working on systems software verification. Current projects focus on making verification more practical and usable by engineers and on leveraging advanced reasoning techniques to tackle complex software. Andrea’s website has more details on his research profile.

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 7 papers accepted to POPL 2024.  This is the seventh year in a row that MPI-SWS researchers have published 5+ papers in POPL.  Congratulations to all our POPL authors!

• Decision and Complexity of Dolev-Yao Hyperproperties by Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind
• Parikh's Theorem Made Symbolic by Matthew Hague, Artur Jez, Anthony Widjaja Lin
• Positive Almost-Sure Termination – Complexity and Proof Rules by Rupak Majumdar and V.R. Sathiyanarayana.
• Ramsey Quantifiers in Linear Arithmetics by Pascal Bergsträßer, Moses Ganardi, Anthony Widjaja Lin, Georg Zetzsche
• Reachability in Continuous Pushdown VASS by A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
• Regular Abstractions for Array Systems by Chih-Duo Hong and Anthony Widjaja Lin
• Securing Verified IO Programs Against Unverified Code in F* by Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter