Federico Poli

Hi! I’m a protocol engineer at Repyh Labs in Zurich. My interests revolve around Rust, distributed systems, automated reasoning, and machine learning.

I recently completed my PhD at ETH Zurich, where I conducted research in the Programming Methodology Group under the supervision of Peter Müller (my main advisor) and Alexander J. Summers. My doctoral work focused on automated reasoning applied to the Rust language, creating tools for bug identification and ensuring software correctness. This involved extensive work in software verification, static analysis, compilers, and Rust language semantics. Notably, I am a co-creator of Prusti, an automated verifier for Rust software that we started developing in 2017.

My professional experience includes internships at AWS, focusing on automated reasoning, and at Google, where I worked on self-supervised machine learning.

Contacts:

• Email
• GitHub
• Google Scholar
• LinkedIn

Projects

• Prusti — our automated verifier for Rust.
• Prusti Assistant — an IDE extension to verify Rust programs in VS Code.
• Mendel — another Rust verifier, specialized in verifying usages of interior mutability.

Talks

• “Building User-Friendly Rust Verification Tools.” At the Rust Verification Workshop, 2024. [Slides]
• “Prusti: Deductive Verification for Rust.” At the Swiss Verification Day, 2024. [Slides] [Demo]
• “Verifying Safe Rust Clients of Internally-Unsafe Libraries.” At the Rust Verification Workshop, 2023. [Slides]
• “Leveraging Rust Types for Modular Specification and Verification.” At Object-​Oriented Programming Systems, Languages, and Applications (OOPSLA), 2019. [Talk]

Publications

† = All authors are listed in alphabetical order.

• “Reasoning about Interior Mutability in Rust using Library-Defined Capabilities.” Federico Poli, Xavier Denis, Peter Müller, Alexander J. Summers. [arXiv]
• † “The Prusti Project: Formal Verification for Rust (invited).” Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers. In NASA Formal Methods (14th International Symposium), 2022. [PDF] [BIB] [DOI]
• † “How do Programmers Use Unsafe Rust?” Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers. In Object-​Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020. [PDF] [BIB] [DOI]
  • Software artifact: [DOI]
• † “Leveraging Rust Types for Modular Specification and Verification.” Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers. In Object-​Oriented Programming Systems, Languages, and Applications (OOPSLA), 2019. [PDF] [BIB] [DOI]
  • Distinguished artifact award
  • Software artifact: [DOI]
  • Extended technical report: [PDF] [BIB] [DOI]