Federico Poli

Hi! I am a PhD candidate in the Programming Methodology Group at ETH Zurich, working under the guidance of Peter Müller (my main advisor) and Alexander J. Summers. My doctoral research focuses on automated reasoning, creating tools to identify bugs and guarantee software correctness. This work spans various aspects of 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 have been actively developing since 2017.

Apart from my doctorate, I have industry experience with machine learning (deep neural networks, Tensorflow), distributed systems (Apache Spark), Python and Java. See my LinkedIn profile, or contact me for a CV.

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

† = The authors are listed in alphabetical order.

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