Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

A Framework for Debugging Automated Program Verification Proofs via Proof Actions. - Chanhee Cho; Yi Zhou 025; Jay Bosamiya; Bryan Parno (CAV (1), 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

Crabtree: Rust API Test Synthesis Guided by Coverage and Type. - Yoshiki Takashima; Chanhee Cho; Ruben Martins; Limin Jia 001; Corina S. Pasareanu (Proc. ACM Program. Lang., 2024)