Zachary Tatlock

According to our database, Zachary Tatlock authored at least 46 papers between 2008 and 2021.

Collaborative distances:

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

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

2020

Dynamic Tensor Rematerialization.

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

CoRR, 2020

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

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

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

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