Zachary Tatlock

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