Youssef's website

This page contains more detailed information on my research experience, presentations and awards.

research experience

• Supervisor: Dr. Alexander J. Summers, funded by UBC EnSURE
• Developing a new prototype implementation of Mendel, a technique for verifying clients of interior-mutable Rust modules that uses implicit capabilities describing the access permissions granted by the design of module APIs.
• Characterizing the interaction between Mendel’s implicit capability model and the place capability information exposed by Place Capability Graphs, a state-of-the-art model of the Rust compiler’s type checking results.

• Supervisor: Dr. Alexander J. Summers, partially funded by UBC SURE
• Designed and implemented a novel encoder for Prusti, a Viper-based Rust verifier, using only pure assertions to eliminate modelling heap memory explicitly for quicker, more efficient verification.
• Rewrote function call modelling for Place Capability Graphs to produce a more precise representation of Rust references and reborrowing semantics.

• Supervisor: Dr. Mark Greenstreet
• Mechanized and proved structural properties of Huffman-tree depth-first search algorithms in ACL2, developing proof strategies toward establishing equivalence between tail-recursive and non-tail-recursive versions.

presentations

Youssef Saleh, Zachary Grannan, Alexander Summers. Optimized Verification Condition Generation for Rust Verification. August 2025. Poster: UBC Computer Science Summer USRA Poster Event, Vancouver, BC, Canada.

awards