Yuyan Bao

28 papers A* 3B 3Journal 20Unranked 2
YearRankTypeTitle / Venue / Authors
2025 J jnl
Complete the Cycle: Reachability Types with Expressive Cyclic References.
CoRR
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
2025 J jnl
Complete the Cycle: Reachability Types with Expressive Cyclic References.
Proc. ACM Program. Lang.
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
2025 J jnl
Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer.
CoRR
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
2025 J jnl
Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory.
Proc. ACM Program. Lang.
Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bracevac, Tiark Rompf
2025 J jnl
Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness.
CoRR
Yuyan Bao, Tiark Rompf
2025 J jnl
Typestate via Revocable Capabilities.
CoRR
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf
2025 J jnl
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking.
CoRR
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
2024 J jnl
Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking.
CoRR
Songlin Jia, Guannan Wei, Siyuan He, Yueyang Tang, Yuyan Bao, Tiark Rompf
2024 J jnl
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs.
Proc. ACM Program. Lang.
Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, Tiark Rompf
2023 J jnl
Graph IRs for Impure Higher-Order Languages (Technical Report).
CoRR
Oliver Bracevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf
2023 J jnl
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies.
Proc. ACM Program. Lang.
Oliver Bracevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf
2023 J jnl
Modeling Reachability Types with Logical Relations.
CoRR
Yuyan Bao, Guannan Wei, Oliver Bracevac, Tiark Rompf
2023 J jnl
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs.
CoRR
Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, Tiark Rompf
2022 B conf
Bounded Model Checking for LLVM.
FMCAD
Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel
2022 A* conf
Cache Refinement Type for Side-Channel Detection of Cryptographic Software.
CCS
Ke Jiang, Yuyan Bao, Shuai Wang, Zhibo Liu, Tianwei Zhang
2022 J jnl
Cache Refinement Type for Side-Channel Detection of Cryptographic Software.
CoRR
Ke Jiang, Yuyan Bao, Shuai Wang, Zhibo Liu, Tianwei Zhang
2022 A* conf
SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications.
SP
Zhibo Liu, Yuanyuan Yuan, Shuai Wang, Yuyan Bao
2022 J jnl
Verifying verified code.
Innov. Syst. Softw. Eng.
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021 B conf
HACCLE: metaprogramming for secure multi-party computation.
GPCE
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, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni
2021 J jnl
Reachability types: tracking aliasing and separation in higher-order functional programs.
Proc. ACM Program. Lang.
Yuyan Bao, Guannan Wei, Oliver Bracevac, Yuxuan Jiang, Qiyang He, Tiark Rompf
2021 B conf
Verifying Verified Code.
ATVA
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021 J jnl
Verifying Verified Code.
CoRR
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2020 J jnl
HACCLE: An Ecosystem for Building Secure Multi-Party Computations.
CoRR
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni
2019 A* conf
Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation.
USENIX Security Symposium
Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, Dinghao Wu
2019 J jnl
Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation.
CoRR
Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, Dinghao Wu
2018 — conf
A Methodology for Invariants, Framing, and Subtyping in JML.
Principled Software Development
Yuyan Bao, Gary T. Leavens
2018 J jnl
Unifying separation logic and region logic to allow interoperability.
Formal Aspects Comput.
Yuyan Bao, Gary T. Leavens, Gidon Ernst
2015 — conf
Conditional effects in fine-grained region logic.
FTfJP@ECOOP
Yuyan Bao, Gary T. Leavens, Gidon Ernst