Zachary Tatlock

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 70

Top Topics

Distributed Systems

Top Venues

Proc. ACM Program. Lang.

Publications

Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Andrew Cheung, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. ACM Trans. Design Autom. Electr. Syst. 29 (2) (2024)
Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase, René Just, Gilbert Louis Bernstein, Zachary Tatlock
FPGA Technology Mapping Using Sketch-Guided Program Synthesis. ASPLOS (2) (2024)
Edward Misback, Zachary Tatlock, Steven L. Tanimoto
Magic Markup: Maintaining Document-External Markup with an LLM. Programming (2024)
Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase, René Just, Gilbert Louis Bernstein, Zachary Tatlock
FPGA Technology Mapping Using Sketch-Guided Program Synthesis. CoRR (2024)
Gus Henry Smith, Zachary D. Sisco, Thanawat Techaumnuaiwit, Jingtao Xia, Vishal Canumalla, Andrew Cheung, Zachary Tatlock, Chandrakana Nandi, Jonathan Balkind
There and Back Again: A Netlist's Tale with Much Egraphin'. CoRR (2024)
Edward Misback, Zachary Tatlock, Steven L. Tanimoto
Magic Markup: Maintaining Document-External Markup with an LLM. CoRR (2024)
Edward Misback, Caleb Chan, Brett Saiki, Eunice Jun, Zachary Tatlock, Pavel Panchekha
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. CoRR (2023)
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
Better Together: Unifying Datalog and Equality Saturation. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi
Equality Saturation Theory Exploration à la Carte. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
Better Together: Unifying Datalog and Equality Saturation. CoRR (2023)
Amy Zhu, Adriana Schulz, Zachary Tatlock
Exploring Self-Embedded Knitting Programs with Twine. FARM (2023)
Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, René Just, Zachary Tatlock
Generate Compilers from Hardware Models! CoRR (2023)
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
babble: Learning Better Abstractions with E-Graphs and Anti-unification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Edward Misback, Caleb C. Chan, Brett Saiki, Eunice Jun, Zachary Tatlock, Pavel Panchekha
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. UIST (2023)
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
Co-Optimization of Design and Fabrication Plans for Carpentry. ACM Trans. Graph. 41 (3) (2022)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP (2022)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Thierry Tambe, Gus Henry Smith, Akash Gaonkar, Vishal Canumalla, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik
Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface. CoRR (2022)
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha
Small Proofs from Congruence Closure. CoRR (2022)
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
babble: Learning Better Abstractions with E-Graphs and Anti-Unification. CoRR (2022)
Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock
Relational e-matching. Proc. ACM Program. Lang. 6 (POPL) (2022)
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha
Small Proofs from Congruence Closure. FMCAD (2022)
Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock
Dynamic Tensor Rematerialization. ICLR (2021)
Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock
Relational E-Matching. CoRR (2021)
Ganesh Gopalakrishnan, Ignacio Laguna, Ang Li, Pavel Panchekha, Cindy Rubio-González, Zachary Tatlock
Guarding Numerics Amidst Rising Heterogeneity. Correctness@SC (2021)
Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock
Combining Precision Tuning and Rewriting. ARITH (2021)
Haichen Shen, Jared Roesch, Zhi Chen, Wei Chen, Yong Wu, Mu Li, Vin Sharma, Zachary Tatlock, Yida Wang
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference. MLSys (2021)
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
Co-Optimization of Design and Fabrication Plans for Carpentry: Supplemental Material. CoRR (2021)
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael B. Taylor, Luis Ceze, Zachary Tatlock
Pure tensor program rewriting via access patterns (representation pearl). MAPS@PLDI (2021)
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael B. Taylor, Luis Ceze, Zachary Tatlock
Pure Tensor Program Rewriting via Access Patterns (Representation Pearl). CoRR (2021)
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
Co-Optimization of Design and Fabrication Plans for Carpentry. CoRR (2021)
Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock
Rewrite Rule Inference Using Equality Saturation. CoRR (2021)
Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock
Rewrite rule inference using equality saturation. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha
egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5 (POPL) (2021)
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
QED at Large: A Survey of Engineering of Formally Verified Software. CoRR (2020)
Haichen Shen, Jared Roesch, Zhi Chen, Wei Chen, Yong Wu, Mu Li, Vin Sharma, Zachary Tatlock, Yida Wang
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference. CoRR (2020)
Max Willsey, Yisu Remy Wang, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock
egg: Easy, Efficient, and Extensible E-graphs. CoRR (2020)
Pavel Panchekha, Zachary Tatlock
Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench. VSTTE (2020)
Gus Smith, Zachary Tatlock, Luis Ceze
Enumerating Hardware-Software Splits with Program Rewriting. CoRR (2020)
Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock
Dynamic Tensor Rematerialization. CoRR (2020)
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock
Synthesizing structured CAD models with equality saturation and inverse transformations. PLDI (2020)
Chandrakana Nandi, Adam Anderson, Max Willsey, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock
Using E-Graphs for CAD Parameter Inference. CoRR (2019)
Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Modular verification of web page layout. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, Adriana Schulz
Carpentry compiler. ACM Trans. Graph. 38 (6) (2019)
Jared Roesch, Steven Lyubomirsky, Marisa Kirisame, Josh Pollock, Logan Weber, Ziheng Jiang, Tianqi Chen, Thierry Moreau, Zachary Tatlock
Relay: A High-Level IR for Deep Learning. CoRR (2019)
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. 5 (2-3) (2019)
Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock
Teaching Rigorous Distributed Systems With Efficient Model Checking. EuroSys (2019)
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. CAV (2) (2019)
Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock
Theia: automatically generating correct program state visualizations. SPLASH-E (2019)
David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock
Toward Multi-Precision, Multi-Format Numerics. CORRECTNESS@SC (2019)
Ilya Sergey, James R. Wilcox, Zachary Tatlock
Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2 (POPL) (2018)
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Finding root causes of floating point error. PLDI (2018)
Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Verifying that web pages have accessible layout. PLDI (2018)
Doug Woos, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson
A Graphical Interactive Debugger for Distributed Systems. CoRR (2018)
Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock
Relay: A New IR for Machine Learning Frameworks. CoRR (2018)
Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock
Relay: a new IR for machine learning frameworks. MAPL@PLDI (2018)
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman
Œuf: minimizing the Coq extraction TCB. CPP (2018)
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
Combining Tools for Optimization and Analysis of Floating-Point Computations. FM (2018)
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
Combining Tools for Optimization and Analysis of Floating-Point Computations. CoRR (2018)
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). ITP (2018)
Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, Zachary Tatlock
Functional programming for compiling and decompiling computer-aided design. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
SpaceSearch: a library for building and verifying solver-aided tools. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Finding Root Causes of Floating Point Error with Herbgrind. CoRR (2017)
James R. Wilcox, Ilya Sergey, Zachary Tatlock
Programming Language Abstractions for Modularly Verified Distributed Systems. SNAPL (2017)
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
Programming Language Tools and Techniques for 3D Printing. SNAPL (2017)
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
Scalable verification of border gateway protocol configurations with an SMT solver. OOPSLA (2016)
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. CAV (2) (2016)
Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock
Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. NSV@CAV (2016)
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson
Planning for change in a formal verification of the raft consensus protocol. CPP (2016)
Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
Verified peephole optimizations for CompCert. PLDI (2016)
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
Toward a Dependability Case Language and Workflow for a Radiation Therapy System. SNAPL (2015)
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
Automatically improving accuracy for floating point expressions. PLDI (2015)
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
Visual Robot Programming for Generalizable Mobile Manipulation Tasks. HRI (Extended Abstracts) (2015)
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
RoboFlow: A flow-based visual programming language for mobile manipulation tasks. ICRA (2015)
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, Thomas E. Anderson
Verdi: a framework for implementing and formally verifying distributed systems. PLDI (2015)
Dongseok Jang, Zachary Tatlock, Sorin Lerner
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. NDSS (2014)
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI (2014)
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
Automating formal proofs for reactive systems. PLDI (2014)
Dongseok Jang, Zachary Tatlock, Sorin Lerner
Establishing Browser Security Guarantees through Formal Shim Verification. USENIX Security Symposium (2012)
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Equality Saturation: A New Approach to Optimization Log. Methods Comput. Sci. 7 (1) (2011)
Zachary Tatlock, Sorin Lerner
Bringing extensibility to verified compilers. PLDI (2010)
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Proving optimizations correct using parameterized program equivalence. PLDI (2009)
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Equality saturation: a new approach to optimization. POPL (2009)
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
Deep typechecking and refactoring. OOPSLA (2008)