Conditional effects in fine-grained region logic. - Yuyan Bao; Gary T. Leavens; Gidon Ernst (FTfJP@ECOOP, 2015)

A Methodology for Invariants, Framing, and Subtyping in JML. - Yuyan Bao; Gary T. Leavens (Principled Software Development, 2018)

Unifying separation logic and region logic to allow interoperability. - Yuyan Bao; Gary T. Leavens; Gidon Ernst (Formal Aspects Comput., 2018)

Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation. - Shuai Wang 011; Yuyan Bao; Xiao Liu 025; Pei Wang 007; Danfeng Zhang; Dinghao Wu (USENIX Security Symposium, 2019)

HACCLE: An Ecosystem for Building Secure Multi-Party Computations. - Yuyan Bao; Kirshanthan Sundararajah; Raghav Malik; Qianchuan Ye; Christopher Wagner; Fei Wang 046; Mohammad Hassan Ameri; Donghang Lu; Alexander Seto; Benjamin Delaware; Roopsha Samanta; Aniket Kate; et al. (CoRR, 2020)

HACCLE: metaprogramming for secure multi-party computation. - Yuyan Bao; Kirshanthan Sundararajah; Raghav Malik; Qianchuan Ye; Christopher Wagner; Nouraldin Jaber; Fei Wang 046; Mohammad Hassan Ameri; Donghang Lu; Alexander Seto; Benjamin Delaware; Roopsha Samanta; et al. (GPCE, 2021)

Reachability types: tracking aliasing and separation in higher-order functional programs. - Yuyan Bao; Guannan Wei 001; Oliver Bracevac; Yuxuan Jiang 006; Qiyang He; Tiark Rompf (Proc. ACM Program. Lang., 2021)

Cache Refinement Type for Side-Channel Detection of Cryptographic Software. - Ke Jiang; Yuyan Bao; Shuai Wang 011; Zhibo Liu; Tianwei Zhang 004 (CCS, 2022)

Bounded Model Checking for LLVM. - Siddharth Priya; Yusen Su; Yuyan Bao; Xiang Zhou; Yakir Vizel; Arie Gurfinkel (FMCAD, 2022)

SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications. - Zhibo Liu; Yuanyuan Yuan; Shuai Wang 011; Yuyan Bao (SP, 2022)

Verifying verified code. - Siddharth Priya; Xiang Zhou; Yusen Su; Yakir Vizel; Yuyan Bao; Arie Gurfinkel (Innov. Syst. Softw. Eng., 2022)

Modeling Reachability Types with Logical Relations. - Yuyan Bao; Guannan Wei 001; Oliver Bracevac; Tiark Rompf (CoRR, 2023)

Graph IRs for Impure Higher-Order Languages (Technical Report). - Oliver Bracevac; Guannan Wei 001; Songlin Jia; Supun Abeysinghe; Yuxuan Jiang 006; Yuyan Bao; Tiark Rompf (CoRR, 2023)

Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies. - Oliver Bracevac; Guannan Wei 001; Songlin Jia; Supun Abeysinghe; Yuxuan Jiang 006; Yuyan Bao; Tiark Rompf (Proc. ACM Program. Lang., 2023)

Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking. - Songlin Jia; Guannan Wei 001; Siyuan He; Yueyang Tang; Yuyan Bao; Tiark Rompf (CoRR, 2024)

Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. - Guannan Wei 001; Oliver Bracevac; Songlin Jia; Yuyan Bao; Tiark Rompf (Proc. ACM Program. Lang., 2024)

Complete the Cycle: Reachability Types with Expressive Cyclic References. - Haotian Deng 001; Siyuan He; Songlin Jia; Yuyan Bao; Tiark Rompf (CoRR, 2025)