| Verdi: A framework for formally verifying distributed system implementations JR Wilcox, D Woos, P Panchekha, Z Tatlock, X Wang, MD Ernst, ... Proceedings of the 2015 ACM SIGPLAN Conference on Programming Language …, 2015 | 442* | 2015 |
| Equality saturation: a new approach to optimization R Tate, M Stepp, Z Tatlock, S Lerner Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009 | 330 | 2009 |
| Automatically improving accuracy for floating point expressions P Panchekha, A Sanchez-Stern, JR Wilcox, Z Tatlock Acm Sigplan Notices 50 (6), 1-11, 2015 | 273 | 2015 |
| Egg: Fast and extensible equality saturation M Willsey, C Nandi, YR Wang, O Flatt, Z Tatlock, P Panchekha Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 210 | 2021 |
| SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. D Jang, Z Tatlock, S Lerner NDSS, 2014 | 203 | 2014 |
| RoboFlow: A flow-based visual programming language for mobile manipulation tasks S Alexandrova, Z Tatlock, M Cakmak 2015 IEEE International Conference on Robotics and Automation (ICRA), 5537-5544, 2015 | 178 | 2015 |
| Planning for change in a formal verification of the raft consensus protocol D Woos, JR Wilcox, S Anton, Z Tatlock, MD Ernst, T Anderson Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 167 | 2016 |
| Relay: A new ir for machine learning frameworks J Roesch, S Lyubomirsky, L Weber, J Pollock, M Kirisame, T Chen, ... Proceedings of the 2nd ACM SIGPLAN international workshop on machine …, 2018 | 161* | 2018 |
| Proving optimizations correct using parameterized program equivalence S Kundu, Z Tatlock, S Lerner ACM Sigplan Notices 44 (6), 327-337, 2009 | 157 | 2009 |
| Programming and proving with distributed protocols I Sergey, JR Wilcox, Z Tatlock Proceedings of the ACM on Programming Languages 2 (POPL), 1-30, 2017 | 154 | 2017 |
| Synthesizing structured CAD models with equality saturation and inverse transformations C Nandi, M Willsey, A Anderson, JR Wilcox, E Darulova, D Grossman, ... Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020 | 101 | 2020 |
| QED at large: A survey of engineering of formally verified software T Ringer, K Palmskog, I Sergey, M Gligoric, Z Tatlock Foundations and Trends® in Programming Languages 5 (2-3), 102-281, 2019 | 97 | 2019 |
| Establishing browser security guarantees through formal shim verification D Jang, Z Tatlock, S Lerner 21st USENIX Security Symposium (USENIX Security 12), 113-128, 2012 | 94 | 2012 |
| Jitk: A Trustworthy {In-Kernel} Interpreter Infrastructure X Wang, D Lazar, N Zeldovich, A Chlipala, Z Tatlock 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2014 | 91 | 2014 |
| Dynamic tensor rematerialization M Kirisame, S Lyubomirsky, A Haan, J Brennan, M He, J Roesch, T Chen, ... arXiv preprint arXiv:2006.09616, 2020 | 89 | 2020 |
| Scalable verification of border gateway protocol configurations with an SMT solver K Weitz, D Woos, E Torlak, MD Ernst, A Krishnamurthy, Z Tatlock Proceedings of the 2016 acm sigplan international conference on object …, 2016 | 88 | 2016 |
| Finding root causes of floating point error A Sanchez-Stern, P Panchekha, S Lerner, Z Tatlock Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018 | 87* | 2018 |
| Toward a standard benchmark format and suite for floating-point analysis N Damouche, M Martel, P Panchekha, C Qiu, A Sanchez-Stern, Z Tatlock Numerical Software Verification: 9th International Workshop, NSV 2016 …, 2017 | 77 | 2017 |
| Œuf: minimizing the Coq extraction TCB E Mullen, S Pernsteiner, JR Wilcox, Z Tatlock, D Grossman Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 70 | 2018 |
| Verified peephole optimizations for CompCert E Mullen, D Zuniga, Z Tatlock, D Grossman Proceedings of the 37th ACM SIGPLAN Conference on Programming Language …, 2016 | 65 | 2016 |
Pavel PanchekhaUniversity of Utah, Kahlert School of ComputingEmail verificata su cs.utah.edu