| Understanding the mirai botnet M Antonakakis, T April, M Bailey, M Bernhard, E Bursztein, J Cochran, ... 26th USENIX security symposium (USENIX Security 17), 1093-1110, 2017 | 3222 | 2017 |
| Verus: Verifying rust programs using linear ghost types A Lattuada, T Hance, C Cho, M Brun, I Subasinghe, Y Zhou, J Howell, ... Proceedings of the ACM on Programming Languages 7 (OOPSLA1), 286-315, 2023 | 167 | 2023 |
| Erays: reverse engineering ethereum's opaque smart contracts Y Zhou, D Kumar, S Bakshi, J Mason, A Miller, M Bailey 27th USENIX security symposium (USENIX Security 18), 1371-1385, 2018 | 161 | 2018 |
| A security model and fully verified implementation for the IETF QUIC record layer A Delignat-Lavaud, C Fournet, B Parno, J Protzenko, T Ramananandro, ... 2021 IEEE Symposium on Security and Privacy (SP), 1162-1178, 2021 | 47 | 2021 |
| Linear types for large-scale systems verification J Li, A Lattuada, Y Zhou, J Cameron, J Howell, B Parno, C Hawblitzel Proceedings of the ACM on Programming Languages 6 (OOPSLA1), 1-28, 2022 | 38 | 2022 |
| Mariposa: Measuring SMT Instability in Automated Program Verification Y Zhou, J Bosamiya, Y Takashima, J Li, M Heule, B Parno Formal Methods in Computer-Aided Design, 2023, 178-188, 2023 | 25 | 2023 |
| Sharding the state machine: Automated modular reasoning for complex concurrent systems T Hance, Y Zhou, A Lattuada, R Achermann, A Conway, R Stutsman, ... 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2023 | 24 | 2023 |
| Context Pruning for More Robust SMT-based Program Verification Y Zhou, J Bosamiya, JG Li, MJH Heule, B Parno Formal Methods in Computer-Aided Design, 2024, 59-69, 2024 | 13 | 2024 |
| A framework for debugging automated program verification proofs via proof actions C Cho, Y Zhou, J Bosamiya, B Parno International Conference on Computer Aided Verification, 348-361, 2024 | 11 | 2024 |
| Verus: verifying Rust programs using linear ghost types (extended version) A Lattuada, T Hance, C Cho, M Brun, I Subasinghe, Y Zhou, J Howell, ... arXiv preprint arXiv:2303.05491, 2023 | 8 | 2023 |
| Cazamariposas: Automated instability debugging in smt-based program verification Y Zhou, A Shah, Z Lin, M Heule, B Parno Conference on Automated Deduction 122, 2025 | 5 | 2025 |
| Galápagos: Developing verified low level cryptography on heterogeneous hardwares Y Zhou, S Gibson, S Cai, M Winchell, B Parno Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications …, 2023 | 5 | 2023 |
| Mariposa: Measuring SMT Instability in Automated Program Verification (Technical Report) Y Zhou, J Bosamiya, Y Takashima, J Li, M Heule, B Parno Carnegie Mellon University, 2023 | 2 | 2023 |
| Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (Technical Report) Y Zhou, A Shah, Z Lin, M Heule, B Parno Carnegie Mellon University, 0 | 1 | |
