Flexible Refinement Proofs in Separation Logic. - Aurel Bílý; Christoph Matheja; Peter Müller 001 (CoRR, 2021)

Modular specification and verification of closures in Rust. - Fabian Wolff; Aurel Bílý; Christoph Matheja; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

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)

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. - Aurel Bílý; Jonas Hansen; Peter Müller 001; Alexander J. Summers (CoRR, 2022)

Refinement Proofs in Rust Using Ghost Locks. - Aurel Bílý; João C. Pereira; Jan Schär; Peter Müller 001 (CoRR, 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)