Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor. - Zhenyang Dai; Shuang Liu; Vilhelm Sjöberg; Xupeng Li; Yu Chen 004; Wenhao Wang 001; Yuekai Jia; Sean Noble Anderson; Laila Elbeheiry; Shubham Sondhi; Yu Zhang; Zhaozhong Ni; et al. (ASPLOS (2), 2024)

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers. - Kimaya Bedarkar; Laila Elbeheiry; Michael Sammler; Lennard Gäher; Björn B. Brandenburg; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2025)

Data Race Freedom à la Mode. - Aïna Linn Georges; Benjamin Peters; Laila Elbeheiry; Leo White; Stephen Dolan; Richard A. Eisenberg; Chris Casinghino; François Pottier; Derek Dreyer (Proc. ACM Program. Lang., 2025)