Deep typechecking and refactoring. - Zachary Tatlock; Chris Tucker; David Shuffelton; Ranjit Jhala; Sorin Lerner (OOPSLA, 2008)

Proving optimizations correct using parameterized program equivalence. - Sudipta Kundu; Zachary Tatlock; Sorin Lerner (PLDI, 2009)

Bringing extensibility to verified compilers. - Zachary Tatlock; Sorin Lerner (PLDI, 2010)

Equality Saturation: A New Approach to Optimization - Ross Tate; Michael Stepp; Zachary Tatlock; Sorin Lerner (Log. Methods Comput. Sci., 2011)

Establishing Browser Security Guarantees through Formal Shim Verification. - Dongseok Jang; Zachary Tatlock; Sorin Lerner (USENIX Security Symposium, 2012)

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. - Dongseok Jang; Zachary Tatlock; Sorin Lerner (NDSS, 2014)

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. - Xi Wang 005; David Lazar; Nickolai Zeldovich; Adam Chlipala; Zachary Tatlock (OSDI, 2014)

Automating formal proofs for reactive systems. - Daniel Ricketts 001; Valentin Robert; Dongseok Jang; Zachary Tatlock; Sorin Lerner (PLDI, 2014)

Reducing the Costs of Proof Assistant Based Formal Verification or : Conviction without the Burden of Proof. - Zachary Tatlock (2014)

Visual Robot Programming for Generalizable Mobile Manipulation Tasks. - Sonya Alexandrova; Zachary Tatlock; Maya Cakmak (HRI (Extended Abstracts), 2015)

RoboFlow: A flow-based visual programming language for mobile manipulation tasks. - Sonya Alexandrova; Zachary Tatlock; Maya Cakmak (ICRA, 2015)

Automatically improving accuracy for floating point expressions. - Pavel Panchekha; Alex Sanchez-Stern; James R. Wilcox; Zachary Tatlock (PLDI, 2015)

Verdi: a framework for implementing and formally verifying distributed systems. - James R. Wilcox; Doug Woos; Pavel Panchekha; Zachary Tatlock; Xi Wang 005; Michael D. Ernst; Thomas E. Anderson (PLDI, 2015)

Toward a Dependability Case Language and Workflow for a Radiation Therapy System. - Michael D. Ernst; Dan Grossman; Jon Jacky; Calvin Loncaric; Stuart Pernsteiner; Zachary Tatlock; Emina Torlak; Xi Wang 005 (SNAPL, 2015)

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. - Nasrine Damouche; Matthieu Martel; Pavel Panchekha; Chen Qiu; Alexander Sanchez-Stern; Zachary Tatlock (NSV@CAV, 2016)

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. - Stuart Pernsteiner; Calvin Loncaric; Emina Torlak; Zachary Tatlock; Xi Wang 005; Michael D. Ernst; Jonathan Jacky (CAV (2), 2016)

Planning for change in a formal verification of the raft consensus protocol. - Doug Woos; James R. Wilcox; Steve Anton; Zachary Tatlock; Michael D. Ernst; Thomas E. Anderson (CPP, 2016)

Scalable verification of border gateway protocol configurations with an SMT solver. - Konstantin Weitz; Doug Woos; Emina Torlak; Michael D. Ernst; Arvind Krishnamurthy; Zachary Tatlock (OOPSLA, 2016)

Verified peephole optimizations for CompCert. - Eric Mullen; Daryl Zuniga; Zachary Tatlock; Dan Grossman (PLDI, 2016)

Programming Language Tools and Techniques for 3D Printing. - Chandrakana Nandi; Anat Caspi; Dan Grossman; Zachary Tatlock (SNAPL, 2017)

Programming Language Abstractions for Modularly Verified Distributed Systems. - James R. Wilcox; Ilya Sergey; Zachary Tatlock (SNAPL, 2017)

Finding Root Causes of Floating Point Error with Herbgrind. - Alex Sanchez-Stern; Pavel Panchekha; Sorin Lerner; Zachary Tatlock (CoRR, 2017)

SpaceSearch: a library for building and verifying solver-aided tools. - Konstantin Weitz; Steven Lyubomirsky; Stefan Heule; Emina Torlak; Michael D. Ernst; Zachary Tatlock (Proc. ACM Program. Lang., 2017)

Œuf: minimizing the Coq extraction TCB. - Eric Mullen; Stuart Pernsteiner; James R. Wilcox; Zachary Tatlock; Dan Grossman (CPP, 2018)

Combining Tools for Optimization and Analysis of Floating-Point Computations. - Heiko Becker; Pavel Panchekha; Eva Darulova; Zachary Tatlock (FM, 2018)

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). - Ramana Kumar; Eric Mullen; Zachary Tatlock; Magnus O. Myreen (ITP, 2018)

Verifying that web pages have accessible layout. - Pavel Panchekha; Adam T. Geller; Michael D. Ernst; Zachary Tatlock; Shoaib Kamil 001 (PLDI, 2018)

Relay: a new IR for machine learning frameworks. - Jared Roesch; Steven Lyubomirsky; Logan Weber; Josh Pollock; Marisa Kirisame; Tianqi Chen 001; Zachary Tatlock (MAPL@PLDI, 2018)

Finding root causes of floating point error. - Alex Sanchez-Stern; Pavel Panchekha; Sorin Lerner; Zachary Tatlock (PLDI, 2018)

A Graphical Interactive Debugger for Distributed Systems. - Doug Woos; Zachary Tatlock; Michael D. Ernst; Thomas E. Anderson (CoRR, 2018)

Functional programming for compiling and decompiling computer-aided design. - Chandrakana Nandi; James R. Wilcox; Pavel Panchekha; Taylor Blau; Dan Grossman; Zachary Tatlock (Proc. ACM Program. Lang., 2018)

Programming and proving with distributed protocols. - Ilya Sergey; James R. Wilcox; Zachary Tatlock (Proc. ACM Program. Lang., 2018)

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. - Heiko Becker; Eva Darulova; Magnus O. Myreen; Zachary Tatlock (CAV (2), 2019)

Teaching Rigorous Distributed Systems With Efficient Model Checking. - Ellis Michael; Doug Woos; Thomas E. Anderson; Michael D. Ernst; Zachary Tatlock (EuroSys, 2019)

Toward Multi-Precision, Multi-Format Numerics. - David Thien; Bill Zorn; Pavel Panchekha; Zachary Tatlock (CORRECTNESS@SC, 2019)

Theia: automatically generating correct program state visualizations. - Josh Pollock; Jared Roesch; Doug Woos; Zachary Tatlock (SPLASH-E, 2019)

Relay: A High-Level IR for Deep Learning. - Jared Roesch; Steven Lyubomirsky; Marisa Kirisame; Josh Pollock; Logan Weber; Ziheng Jiang; Tianqi Chen 001; Thierry Moreau; Zachary Tatlock (CoRR, 2019)

Using E-Graphs for CAD Parameter Inference. - Chandrakana Nandi; Adam Anderson 004; Max Willsey; James R. Wilcox; Eva Darulova; Dan Grossman; Zachary Tatlock (CoRR, 2019)

QED at Large: A Survey of Engineering of Formally Verified Software. - Talia Ringer; Karl Palmskog; Ilya Sergey; Milos Gligoric 001; Zachary Tatlock (Found. Trends Program. Lang., 2019)

Modular verification of web page layout. - Pavel Panchekha; Michael D. Ernst; Zachary Tatlock; Shoaib Kamil 001 (Proc. ACM Program. Lang., 2019)

Carpentry compiler. - Chenming Wu; Haisen Zhao; Chandrakana Nandi; Jeffrey I. Lipton; Zachary Tatlock; Adriana Schulz (ACM Trans. Graph., 2019)

Synthesizing structured CAD models with equality saturation and inverse transformations. - Chandrakana Nandi; Max Willsey; Adam Anderson 004; James R. Wilcox; Eva Darulova; Dan Grossman; Zachary Tatlock (PLDI, 2020)

Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench. - Pavel Panchekha; Zachary Tatlock (VSTTE, 2020)

Enumerating Hardware-Software Splits with Program Rewriting. - Gus Henry Smith; Zachary Tatlock; Luis Ceze (CoRR, 2020)

egg: Easy, Efficient, and Extensible E-graphs. - Max Willsey; Yisu Remy Wang; Oliver Flatt; Chandrakana Nandi; Pavel Panchekha; Zachary Tatlock (CoRR, 2020)

Combining Precision Tuning and Rewriting. - Brett Saiki; Oliver Flatt; Chandrakana Nandi; Pavel Panchekha; Zachary Tatlock (ARITH, 2021)

Guarding Numerics Amidst Rising Heterogeneity. - Ganesh Gopalakrishnan; Ignacio Laguna; Ang Li 006; Pavel Panchekha; Cindy Rubio-González; Zachary Tatlock (Correctness@SC, 2021)

Dynamic Tensor Rematerialization. - Marisa Kirisame; Steven Lyubomirsky; Altan Haan; Jennifer Brennan; Mike He; Jared Roesch; Tianqi Chen 001; Zachary Tatlock (ICLR, 2021)

Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference. - Haichen Shen; Jared Roesch; Zhi Chen 030; Wei Chen; Yong Wu; Mu Li 003; Vin Sharma; Zachary Tatlock; Yida Wang 003 (MLSys, 2021)

Pure tensor program rewriting via access patterns (representation pearl). - Gus Henry Smith; Andrew Liu; Steven Lyubomirsky; Scott Davidson 004; Joseph McMahan; Michael B. Taylor; Luis Ceze; Zachary Tatlock (MAPS@PLDI, 2021)

Co-Optimization of Design and Fabrication Plans for Carpentry: Supplemental Material. - Haisen Zhao; Max Willsey; Amy Zhu; Chandrakana Nandi; Zachary Tatlock; Justin Solomon 001; Adriana Schulz (CoRR, 2021)

Rewrite rule inference using equality saturation. - Chandrakana Nandi; Max Willsey; Amy Zhu; Yisu Remy Wang; Brett Saiki; Adam Anderson 004; Adriana Schulz; Dan Grossman; Zachary Tatlock (Proc. ACM Program. Lang., 2021)

egg: Fast and extensible equality saturation. - Max Willsey; Chandrakana Nandi; Yisu Remy Wang; Oliver Flatt; Zachary Tatlock; Pavel Panchekha (Proc. ACM Program. Lang., 2021)

Verified Compilation and Optimization of Floating-Point Programs in CakeML. - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (ECOOP, 2022)

Small Proofs from Congruence Closure. - Oliver Flatt; Samuel Coward; Max Willsey; Zachary Tatlock; Pavel Panchekha (FMCAD, 2022)

Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface. - Bo-Yuan Huang 001; Steven Lyubomirsky; Yi Li; Mike He; Thierry Tambe; Gus Henry Smith; Akash Gaonkar; Vishal Canumalla; Gu-Yeon Wei; Aarti Gupta; Zachary Tatlock; Sharad Malik (CoRR, 2022)

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (Dagstuhl Artifacts Ser., 2022)

Relational e-matching. - Yihong Zhang 004; Yisu Remy Wang; Max Willsey; Zachary Tatlock (Proc. ACM Program. Lang., 2022)

Co-Optimization of Design and Fabrication Plans for Carpentry. - Haisen Zhao; Max Willsey; Amy Zhu; Chandrakana Nandi; Zachary Tatlock; Justin Solomon 001; Adriana Schulz (ACM Trans. Graph., 2022)

Exploring Self-Embedded Knitting Programs with Twine. - Amy Zhu; Adriana Schulz; Zachary Tatlock (FARM, 2023)

Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. - Edward Misback; Caleb C. Chan; Brett Saiki; Eunice Jun; Zachary Tatlock; Pavel Panchekha (UIST, 2023)

Generate Compilers from Hardware Models! - Gus Henry Smith; Benjamin Kushigian; Vishal Canumalla; Andrew Cheung; René Just; Zachary Tatlock (CoRR, 2023)

Better Together: Unifying Datalog and Equality Saturation. - Yihong Zhang 004; Yisu Remy Wang; Oliver Flatt; David Cao; Philip Zucker; Eli Rosenthal; Zachary Tatlock; Max Willsey (Proc. ACM Program. Lang., 2023)

babble: Learning Better Abstractions with E-Graphs and Anti-unification. - David Cao; Rose Kunkel; Chandrakana Nandi; Max Willsey; Zachary Tatlock; Nadia Polikarpova (Proc. ACM Program. Lang., 2023)

Equality Saturation Theory Exploration à la Carte. - Anjali Pal; Brett Saiki; Ryan Tjoa; Cynthia Richey; Amy Zhu; Oliver Flatt; Max Willsey; Zachary Tatlock; Chandrakana Nandi (Proc. ACM Program. Lang., 2023)

FPGA Technology Mapping Using Sketch-Guided Program Synthesis. - Gus Henry Smith; Benjamin Kushigian; Vishal Canumalla; Andrew Cheung; Steven Lyubomirsky; Sorawee Porncharoenwase; René Just; Gilbert Louis Bernstein; Zachary Tatlock (ASPLOS (2), 2024)

Magic Markup: Maintaining Document-External Markup with an LLM. - Edward Misback; Zachary Tatlock; Steven L. Tanimoto (Programming, 2024)

There and Back Again: A Netlist's Tale with Much Egraphin'. - Gus Henry Smith; Zachary D. Sisco; Thanawat Techaumnuaiwit; Jingtao Xia; Vishal Canumalla; Andrew Cheung; Zachary Tatlock; Chandrakana Nandi; Jonathan Balkind (CoRR, 2024)

Scaling Program Synthesis Based Technology Mapping with Equality Saturation. - Gus Henry Smith; Colin Knizek; Daniel Petrisko; Zachary Tatlock; Jonathan Balkind; Gilbert Louis Bernstein; Haobin Ni; Chandrakana Nandi (CoRR, 2024)

Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. - Bo-Yuan Huang 001; Steven Lyubomirsky; Yi Li; Mike He; Gus Henry Smith; Thierry Tambe; Akash Gaonkar; Vishal Canumalla; Andrew Cheung; Gu-Yeon Wei; Aarti Gupta; Zachary Tatlock; et al. (ACM Trans. Design Autom. Electr. Syst., 2024)

Computational Illusion Knitting. - Amy Zhu; Yuxuan Mei; Benjamin T. Jones; Zachary Tatlock; Adriana Schulz (ACM Trans. Graph., 2024)

Target-Aware Implementation of Real Expressions. - Brett Saiki; Jackson Brough; Jonas Regehr; Jesús Ponce; Varun Pradeep; Aditya Akhileshwaran; Zachary Tatlock; Pavel Panchekha (ASPLOS (1), 2025)

Codetations: Intelligent, Persistent Notes and UIs for Programs and Other Documents. - Edward Misback; Erik Vank; Zachary Tatlock; Steven L. Tanimoto (CoRR, 2025)