Zachary Tatlock
Cited by
Cited by
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
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
Automatically improving accuracy for floating point expressions
P Panchekha, A Sanchez-Stern, JR Wilcox, Z Tatlock
Acm Sigplan Notices 50 (6), 1-11, 2015
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks.
D Jang, Z Tatlock, S Lerner
NDSS, 2014
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
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
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
Proving optimizations correct using parameterized program equivalence
S Kundu, Z Tatlock, S Lerner
ACM Sigplan Notices 44 (6), 327-337, 2009
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
Programming and proving with distributed protocols
I Sergey, JR Wilcox, Z Tatlock
Proceedings of the ACM on Programming Languages 2 (POPL), 1-30, 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
Establishing browser security guarantees through formal shim verification
D Jang, Z Tatlock, S Lerner
21st USENIX Security Symposium (USENIX Security 12), 113-128, 2012
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
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
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
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
Dynamic tensor rematerialization
M Kirisame, S Lyubomirsky, A Haan, J Brennan, M He, J Roesch, T Chen, ...
arXiv preprint arXiv:2006.09616, 2020
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
Œ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
Verified peephole optimizations for CompCert
E Mullen, D Zuniga, Z Tatlock, D Grossman
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language …, 2016
The system can't perform the operation now. Try again later.
Articles 1–20