Projects
- Prusti — Our automated verifier for Rust. I worked on this from 2017 to 2024.
- Prusti Assistant — An IDE extension to verify Rust programs in VS Code with Prusti. I worked on this from 2017 to 2024.
- Mendel — Another Rust verifier, specialized in verifying usages of interior mutability. I worked on this from 2022 to 2024.
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.
- Doctoral Thesis, “Enabling Rich Lightweight Verification of Rust Software.” Federico Poli. [PDF] [BIB] [DOI]
- “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]