| Identifying {Cache-Based} Side Channels through {Secret-Augmented} Abstract Interpretation S Wang, Y Bao, X Liu, P Wang, D Zhang, D Wu 28th USENIX security symposium (USENIX security 19), 657-674, 2019 | 65 | 2019 |
| Reachability types: tracking aliasing and separation in higher-order functional programs Y Bao, G Wei, O Bračevac, Y Jiang, Q He, T Rompf Proceedings of the ACM on Programming Languages 5 (OOPSLA), 1-32, 2021 | 27 | 2021 |
| Sok: Demystifying binary lifters through the lens of downstream applications Z Liu, Y Yuan, S Wang, Y Bao 2022 IEEE Symposium on Security and Privacy (SP), 1100-1119, 2022 | 22 | 2022 |
| Graph IRS for impure higher-order languages: making aggressive optimizations affordable with precise effect dependencies O Bračevac, G Wei, S Jia, S Abeysinghe, Y Jiang, Y Bao, T Rompf Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 400-430, 2023 | 18 | 2023 |
| Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs G Wei, O Bračevac, S Jia, Y Bao, T Rompf Proceedings of the ACM on Programming Languages 8 (POPL), 393-424, 2024 | 14 | 2024 |
| Verifying verified code S Priya, X Zhou, Y Su, Y Vizel, Y Bao, A Gurfinkel Innovations in Systems and Software Engineering 18 (3), 335-346, 2022 | 13 | 2022 |
| Conditional effects in fine-grained region logic Y Bao, GT Leavens, G Ernst Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs …, 2015 | 10 | 2015 |
| Bounded Model Checking for LLVM. S Priya, Y Su, Y Bao, X Zhou, Y Vizel, A Gurfinkel FMCAD, 214-224, 2022 | 8 | 2022 |
| Unifying separation logic and region logic to allow interoperability Y Bao, GT Leavens, G Ernst Formal Aspects of Computing 30, 381-441, 2018 | 8 | 2018 |
| Cache refinement type for side-channel detection of cryptographic software K Jiang, Y Bao, S Wang, Z Liu, T Zhang Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications …, 2022 | 7 | 2022 |
| HACCLE: metaprogramming for secure multi-party computation Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, N Jaber, F Wang, ... Proceedings of the 20th ACM SIGPLAN International Conference on Generative …, 2021 | 7 | 2021 |
| Graph irs for impure higher-order languages (technical report) O Bračevac, G Wei, S Jia, S Abeysinghe, Y Jiang, Y Bao, T Rompf arXiv preprint arXiv:2309.08118, 2023 | 6 | 2023 |
| Reasoning about frame properties in object-oriented programs Y Bao | 4 | 2017 |
| Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, and Equational Theory Y Bao, G Wei, O Bračevac, T Rompf arXiv preprint arXiv:2309.05885, 2023 | 3 | 2023 |
| A methodology for invariants, framing, and subtyping in JML Y Bao, GT Leavens Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter …, 2018 | 3 | 2018 |
| Translating separation logic into dynamic frames using fine-grained region logic Y Bao, GT Leavens, G Ernst Technical Report CS-TR-13-02a, Computer Science, University of Central …, 2014 | 3 | 2014 |
| HACCLE: An Ecosystem for Building Secure Multi-Party Computations Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, F Wang, MH Ameri, ... arXiv preprint arXiv:2009.01489, 2020 | 1 | 2020 |
| Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking S Jia, G Wei, S He, Y Tang, Y Bao, T Rompf arXiv preprint arXiv:2404.08217, 2024 | | 2024 |
| HACCLE: Metaprogramming for Secure Multi-Party Computation--Extended Version Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, N Jaber, F Wang, ... arXiv preprint arXiv:2009.01489, 2020 | | 2020 |
| Fine-Grained Region Logic Y Bao, GT Leavens, G Ernst | | 2016 |
Tiark RompfPurdue UniversityVerified email at purdue.edu