default search action
Zachary Tatlock
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j17]Bo-Yuan Huang
, Steven Lyubomirsky
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. ACM Trans. Design Autom. Electr. Syst. 29(2): 35:1-35:25 (2024) - [j16]Amy Zhu
Computational Illusion Knitting. ACM Trans. Graph. 43(4): 152:1-152:13 (2024) - [c43]Gus Henry Smith
FPGA Technology Mapping Using Sketch-Guided Program Synthesis. ASPLOS (2) 2024: 416-432 - [c42]Edward Misback
Magic Markup: Maintaining Document-External Markup with an LLM. Programming 2024 - [i25]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 abs/2401.16526 (2024) - [i24]Edward Misback, Zachary Tatlock, Steven L. Tanimoto:
Magic Markup: Maintaining Document-External Markup with an LLM. CoRR abs/2403.03481 (2024) - [i23]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 abs/2404.00786 (2024) - 2023
- [j15]Anjali Pal
Equality Saturation Theory Exploration à la Carte. Proc. ACM Program. Lang. 7(OOPSLA2): 1034-1062 (2023) - [j14]Yihong Zhang
Better Together: Unifying Datalog and Equality Saturation. Proc. ACM Program. Lang. 7(PLDI): 468-492 (2023) - [j13]David Cao
babble: Learning Better Abstractions with E-Graphs and Anti-unification. Proc. ACM Program. Lang. 7(POPL): 396-424 (2023) - [c41]Amy Zhu, Adriana Schulz, Zachary Tatlock:
Exploring Self-Embedded Knitting Programs with Twine. FARM 2023: 25-31 - [c40]Edward Misback
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. UIST 2023: 77:1-77:15 - [i22]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 abs/2304.04332 (2023) - [i21]Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, René Just, Zachary Tatlock:
Generate Compilers from Hardware Models! CoRR abs/2305.09580 (2023) - [i20]Edward Misback, Caleb C. Chan, Brett Saiki, Eunice Jun, Zachary Tatlock, Pavel Panchekha:
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. CoRR abs/2305.10599 (2023) - 2022
- [j12]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): 10:1-10:2 (2022) - [j11]Yihong Zhang
Relational e-matching. Proc. ACM Program. Lang. 6(POPL): 1-22 (2022) - [j10]Haisen Zhao
Co-Optimization of Design and Fabrication Plans for Carpentry. ACM Trans. Graph. 41(3): 32:1-32:13 (2022) - [c39]Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP 2022: 1:1-1:28 - [c38]Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha
Small Proofs from Congruence Closure. FMCAD 2022: 75-83 - [i19]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 abs/2203.00218 (2022) - [i18]Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock
Small Proofs from Congruence Closure. CoRR abs/2209.03398 (2022) - [i17]David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova:
babble: Learning Better Abstractions with E-Graphs and Anti-Unification. CoRR abs/2212.04596 (2022) - 2021
- [j9]Chandrakana Nandi, Max Willsey
Rewrite rule inference using equality saturation. Proc. ACM Program. Lang. 5(OOPSLA): 1-28 (2021) - [j8]Max Willsey
egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) - [c37]Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha
Combining Precision Tuning and Rewriting. ARITH 2021: 1-8 - [c36]Ganesh Gopalakrishnan, Ignacio Laguna, Ang Li, Pavel Panchekha, Cindy Rubio-González, Zachary Tatlock
Guarding Numerics Amidst Rising Heterogeneity. Correctness@SC 2021: 9-15 - [c35]Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock:
Dynamic Tensor Rematerialization. ICLR 2021 - [c34]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 - [c33]Gus Henry Smith
Pure tensor program rewriting via access patterns (representation pearl). MAPS@PLDI 2021: 21-31 - [i16]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 abs/2105.09377 (2021) - [i15]Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz:
Co-Optimization of Design and Fabrication Plans for Carpentry. CoRR abs/2107.12265 (2021) - [i14]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 abs/2107.14745 (2021) - [i13]Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock:
Relational E-Matching. CoRR abs/2108.02290 (2021) - [i12]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 abs/2108.10436 (2021) - 2020
- [c32]Chandrakana Nandi, Max Willsey
Synthesizing structured CAD models with equality saturation and inverse transformations. PLDI 2020: 31-44 - [c31]Pavel Panchekha, Zachary Tatlock
Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench. VSTTE 2020: 213-220 - [i11]Gus Henry Smith, Zachary Tatlock, Luis Ceze:
Enumerating Hardware-Software Splits with Program Rewriting. CoRR abs/2003.00290 (2020) - [i10]Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock:
QED at Large: A Survey of Engineering of Formally Verified Software. CoRR abs/2003.06458 (2020) - [i9]Max Willsey, Yisu Remy Wang, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock:
egg: Easy, Efficient, and Extensible E-graphs. CoRR abs/2004.03082 (2020) - [i8]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 abs/2006.03031 (2020) - [i7]Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock:
Dynamic Tensor Rematerialization. CoRR abs/2006.09616 (2020)
2010 – 2019
- 2019
- [j7]Talia Ringer, Karl Palmskog, Ilya Sergey
QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. 5(2-3): 102-281 (2019) - [j6]Pavel Panchekha, Michael D. Ernst, Zachary Tatlock
Modular verification of web page layout. Proc. ACM Program. Lang. 3(OOPSLA): 151:1-151:26 (2019) - [j5]Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock
Carpentry compiler. ACM Trans. Graph. 38(6): 195:1-195:14 (2019) - [c30]Heiko Becker, Eva Darulova
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. CAV (2) 2019: 155-173 - [c29]Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock
Teaching Rigorous Distributed Systems With Efficient Model Checking. EuroSys 2019: 32:1-32:15 - [c28]David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock
Toward Multi-Precision, Multi-Format Numerics. CORRECTNESS@SC 2019: 19-26 - [c27]Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock
Theia: automatically generating correct program state visualizations. SPLASH-E 2019: 46-56 - [i6]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 abs/1904.08368 (2019) - [i5]Chandrakana Nandi, Adam Anderson, Max Willsey, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock:
Using E-Graphs for CAD Parameter Inference. CoRR abs/1909.12252 (2019) - 2018
- [j4]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): 99:1-99:31 (2018) - [j3]Ilya Sergey
Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL): 28:1-28:30 (2018) - [c26]Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock
Œuf: minimizing the Coq extraction TCB. CPP 2018: 172-185 - [c25]Heiko Becker, Pavel Panchekha, Eva Darulova
Combining Tools for Optimization and Analysis of Floating-Point Computations. FM 2018: 355-363 - [c24]Ramana Kumar, Eric Mullen, Zachary Tatlock
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). ITP 2018: 362-369 - [c23]Pavel Panchekha, Adam T. Geller
Verifying that web pages have accessible layout. PLDI 2018: 1-14 - [c22]Jared Roesch, Steven Lyubomirsky
Relay: a new IR for machine learning frameworks. MAPL@PLDI 2018: 58-68 - [c21]Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Finding root causes of floating point error. PLDI 2018: 256-269 - [i4]Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock:
Combining Tools for Optimization and Analysis of Floating-Point Computations. CoRR abs/1805.02436 (2018) - [i3]Doug Woos, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson:
A Graphical Interactive Debugger for Distributed Systems. CoRR abs/1806.05300 (2018) - [i2]Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock:
Relay: A New IR for Machine Learning Frameworks. CoRR abs/1810.00952 (2018) - 2017
- [j2]Konstantin Weitz, Steven Lyubomirsky
SpaceSearch: a library for building and verifying solver-aided tools. Proc. ACM Program. Lang. 1(ICFP): 25:1-25:28 (2017) - [c20]Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
Programming Language Tools and Techniques for 3D Printing. SNAPL 2017: 10:1-10:12 - [c19]James R. Wilcox, Ilya Sergey
Programming Language Abstractions for Modularly Verified Distributed Systems. SNAPL 2017: 19:1-19:12 - [i1]Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock:
Finding Root Causes of Floating Point Error with Herbgrind. CoRR abs/1705.10416 (2017) - 2016
- [c18]Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. CAV (2) 2016: 23-41 - [c17]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: 63-77 - [c16]Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock
Planning for change in a formal verification of the raft consensus protocol. CPP 2016: 154-165 - [c15]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: 765-780 - [c14]Eric Mullen, Daryl Zuniga, Zachary Tatlock
Verified peephole optimizations for CompCert. PLDI 2016: 448-461 - 2015
- [c13]Sonya Alexandrova, Zachary Tatlock
Visual Robot Programming for Generalizable Mobile Manipulation Tasks. HRI (Extended Abstracts) 2015: 163-164 - [c12]Sonya Alexandrova, Zachary Tatlock
RoboFlow: A flow-based visual programming language for mobile manipulation tasks. ICRA 2015: 5537-5544 - [c11]Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
Automatically improving accuracy for floating point expressions. PLDI 2015: 1-11 - [c10]James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock
Verdi: a framework for implementing and formally verifying distributed systems. PLDI 2015: 357-368 - [c9]Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock
Toward a Dependability Case Language and Workflow for a Radiation Therapy System. SNAPL 2015: 103-112 - 2014
- [b1]Zachary Tatlock:
Reducing the Costs of Proof Assistant Based Formal Verification or : Conviction without the Burden of Proof. University of California, San Diego, USA, 2014 - [c8]Dongseok Jang, Zachary Tatlock, Sorin Lerner:
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. NDSS 2014 - [c7]Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock:
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI 2014: 33-47 - [c6]Daniel Ricketts, Valentin Robert
Automating formal proofs for reactive systems. PLDI 2014: 452-462 - 2012
- [c5]Dongseok Jang, Zachary Tatlock, Sorin Lerner:
Establishing Browser Security Guarantees through Formal Shim Verification. USENIX Security Symposium 2012: 113-128 - 2011
- [j1]Ross Tate
Equality Saturation: A New Approach to Optimization. Log. Methods Comput. Sci. 7(1) (2011) - 2010
- [c4]Zachary Tatlock
Bringing extensibility to verified compilers. PLDI 2010: 111-121
2000 – 2009
- 2009
- [c3]Sudipta Kundu, Zachary Tatlock
Proving optimizations correct using parameterized program equivalence. PLDI 2009: 327-337 - [c2]Ross Tate
Equality saturation: a new approach to optimization. POPL 2009: 264-276 - 2008
- [c1]Zachary Tatlock
Deep typechecking and refactoring. OOPSLA 2008: 37-52
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-04 19:55 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: