Zachary Tatlock

According to our database, Zachary Tatlock authored at least 68 papers between 2008 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface.

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

ACM Trans. Design Autom. Electr. Syst., March, 2024

Magic Markup: Maintaining Document-External Markup with an LLM.

Edward Misback, Zachary Tatlock, Steven L. Tanimoto

CoRR, 2024

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

CoRR, 2024

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., October, 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., January, 2023

Better Together: Unifying Datalog and Equality Saturation.

Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey

Proc. ACM Program. Lang., 2023

Generate Compilers from Hardware Models!

Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, René Just, Zachary Tatlock

CoRR, 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

Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology, 2023

Exploring Self-Embedded Knitting Programs with Twine.

Amy Zhu, Adriana Schulz, Zachary Tatlock

Proceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, 2023

2022

Co-Optimization of Design and Fabrication Plans for Carpentry.

Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz

ACM Trans. Graph., 2022

Relational e-matching.

Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock

Proc. ACM Program. Lang., 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

Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface.

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

CoRR, 2022

Small Proofs from Congruence Closure.

Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

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

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

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

Rewrite rule inference using equality saturation.

Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock

Proc. ACM Program. Lang., 2021

Co-Optimization of Design and Fabrication Plans for Carpentry: Supplemental Material.

Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz

CoRR, 2021

Pure tensor program rewriting via access patterns (representation pearl).

Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael B. Taylor, Luis Ceze, Zachary Tatlock

Proceedings of the MAPS@PLDI 2021: Proceedings of the 5th ACM SIGPLAN International Symposium on Machine Programming, 2021

Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference.

Haichen Shen, Jared Roesch, Zhi Chen, Wei Chen, Yong Wu, Mu Li, Vin Sharma, Zachary Tatlock, Yida Wang

Proceedings of Machine Learning and Systems 2021, 2021

Dynamic Tensor Rematerialization.

Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock

Proceedings of the 9th International Conference on Learning Representations, 2021

Guarding Numerics Amidst Rising Heterogeneity.

Ganesh Gopalakrishnan, Ignacio Laguna, Ang Li, Pavel Panchekha, Cindy Rubio-González, Zachary Tatlock

Proceedings of the 5th IEEE/ACM International Workshop on Software Correctness for HPC Applications, 2021

Combining Precision Tuning and Rewriting.

Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock

Proceedings of the 28th IEEE Symposium on Computer Arithmetic, 2021

2020

egg: Easy, Efficient, and Extensible E-graphs.

Max Willsey, Yisu Remy Wang, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock

CoRR, 2020

Enumerating Hardware-Software Splits with Program Rewriting.

Gus Henry Smith, Zachary Tatlock, Luis Ceze

CoRR, 2020

Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench.

Pavel Panchekha, Zachary Tatlock

Proceedings of the Software Verification - 12th International Conference, 2020

Synthesizing structured CAD models with equality saturation and inverse transformations.

Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

2019

Carpentry compiler.

Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, Adriana Schulz

ACM Trans. Graph., 2019

Modular verification of web page layout.

Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil

Proc. ACM Program. Lang., 2019

QED at Large: A Survey of Engineering of Formally Verified Software.

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock

Found. Trends Program. Lang., 2019

Using E-Graphs for CAD Parameter Inference.

Chandrakana Nandi, Adam Anderson, Max Willsey, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock

CoRR, 2019

Relay: A High-Level IR for Deep Learning.

Jared Roesch, Steven Lyubomirsky, Marisa Kirisame, Josh Pollock, Logan Weber, Ziheng Jiang, Tianqi Chen, Thierry Moreau, Zachary Tatlock

CoRR, 2019

Theia: automatically generating correct program state visualizations.

Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock

Proceedings of the SPLASH-E '19, 2019

Toward Multi-Precision, Multi-Format Numerics.

David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock

Proceedings of the 2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 2019

Teaching Rigorous Distributed Systems With Efficient Model Checking.

Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock

Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, 2019

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.

Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Programming and proving with distributed protocols.

Ilya Sergey, James R. Wilcox, Zachary Tatlock

Proc. ACM Program. Lang., 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

A Graphical Interactive Debugger for Distributed Systems.

Doug Woos, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson

CoRR, 2018

Finding root causes of floating point error.

Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Relay: a new IR for machine learning frameworks.

Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock

Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, 2018

Verifying that web pages have accessible layout.

Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 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

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Combining Tools for Optimization and Analysis of Floating-Point Computations.

Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock

Proceedings of the Formal Methods - 22nd International Symposium, 2018

Œuf: minimizing the Coq extraction TCB.

Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

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

Finding Root Causes of Floating Point Error with Herbgrind.

Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock

CoRR, 2017

Programming Language Abstractions for Modularly Verified Distributed Systems.

James R. Wilcox, Ilya Sergey, Zachary Tatlock

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Programming Language Tools and Techniques for 3D Printing.

Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

2016

Verified peephole optimizations for CompCert.

Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 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

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 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

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.

Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis.

Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock

Proceedings of the Numerical Software Verification - 9th International Workshop, 2016

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

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Verdi: a framework for implementing and formally verifying distributed systems.

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, Thomas E. Anderson

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automatically improving accuracy for floating point expressions.

Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

RoboFlow: A flow-based visual programming language for mobile manipulation tasks.

Sonya Alexandrova, Zachary Tatlock, Maya Cakmak

Proceedings of the IEEE International Conference on Robotics and Automation, 2015

Visual Robot Programming for Generalizable Mobile Manipulation Tasks.

Sonya Alexandrova, Zachary Tatlock, Maya Cakmak

Proceedings of the Tenth Annual ACM/IEEE International Conference on Human-Robot Interaction, 2015

2014

Reducing the Costs of Proof Assistant Based Formal Verification or : Conviction without the Burden of Proof.

Zachary Tatlock

PhD thesis, 2014

Automating formal proofs for reactive systems.

Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure.

Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks.

Dongseok Jang, Zachary Tatlock, Sorin Lerner

Proceedings of the 21st Annual Network and Distributed System Security Symposium, 2014

2012

Establishing Browser Security Guarantees through Formal Shim Verification.

Dongseok Jang, Zachary Tatlock, Sorin Lerner

Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, 2012

2011

Equality Saturation: A New Approach to Optimization

Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner

Log. Methods Comput. Sci., 2011

2010

Bringing extensibility to verified compilers.

Zachary Tatlock, Sorin Lerner

Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

2009

Proving optimizations correct using parameterized program equivalence.

Sudipta Kundu, Zachary Tatlock, Sorin Lerner

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

2008

Deep typechecking and refactoring.

Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner

Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008