Publications
Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf. Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs. [POPL24]
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe , Yuxuan Jiang, Yuyan Bao, Tiark Rompf. Graph IRs for Impure Higher-Order Languages – Making Aggressive Optimizations Affordable with Precise Effect Dependencies. [OOPSLA23]
Ke Jiang, Yuyan Bao, Shuai Wang, Zhibo Liu, Tianwei Zhang. Cache Refinement Type for Side-channel Detection of Cryptographic Software. CCS 2022.
Zhibo Liu, Yuanyuan Yuan, Shuai Wang, Yuyan Bao. SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications. IEEE S&P 2022.
Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf. Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs. [OOPSLA21]
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni. HACCLE: Metaprogramming for Secure Multi-Party Computation. GPCE 2021.
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel. Verifying Verified Code. ATVA 2021: 187-202.
Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, Dinghao Wu. Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation. USENIX Security, 2019.
Yuyan Bao, Gary T. Leavens. A methdology for invariants, framing and subtyping in JML. In Principled Software Development, page 19, 2018.
Yuyan Bao, Gary T. Leavens, Gidon Ernst. Unifying Separation Logic and Region Logic to Allow Interoperability. In Formal Aspect of Computing, pages 1-16, 2018.
Yuyan Bao Gary T. Leavens, Gidon Ernst. Conditional Effects in Fine-Grained Region Logic. FTfJP ‘15