The Prusti Project: Formal Verification for Rust. - Vytautas Astrauskas; Aurel Bílý; Jonás Fiala; Zachary Grannan; Christoph Matheja; Peter Müller 001; Federico Poli 001; Alexander J. Summers (NFM, 2022)

Leveraging Rust Types for Program Synthesis. - Jonás Fiala; Shachar Itzhaky; Peter Müller 001; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2023)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees. - Zachary Grannan; Aurel Bílý; Jonás Fiala; Jasper Geer; Markus de Medeiros; Peter Müller 001; Alexander J. Summers (CoRR, 2025)