Zachary Tatlock
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
34
Venues
19
Active years
2008–2025
Best venue rank
A*
Where they publish
Papers
34 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | ASPLOS | Target-Aware Implementation of Real Expressions. | Brett Saiki, Jackson Brough, Jonas Regehr, Jess Ponce, Varun Pradeep, Aditya Akhileshwaran, Zachary Tatlock, Pavel Panchekha |
| 2024 | ASPLOS | 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 |
| 2023 | UIST | Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting. | Edward Misback, Caleb C. Chan, Brett Saiki, Eunice Jun, Zachary Tatlock, Pavel Panchekha |
| 2022 | ECOOP | 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 |
| 2022 | FMCAD | Small Proofs from Congruence Closure. | Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha |
| 2021 | ARITH | Combining Precision Tuning and Rewriting. | Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock |
| 2021 | ICLR | Dynamic Tensor Rematerialization. | Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock |
| 2021 | PLDI | 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 |
| 2020 | PLDI | 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 |
| 2019 | CAV | Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. | Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock |
| 2019 | EuroSys | Teaching Rigorous Distributed Systems With Efficient Model Checking. | Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock |
| 2019 | SC | Toward Multi-Precision, Multi-Format Numerics. | David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock |
| 2018 | CPP | Œuf: minimizing the Coq extraction TCB. | Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |
| 2018 | FM | Combining Tools for Optimization and Analysis of Floating-Point Computations. | Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock |
| 2018 | ITP | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
| 2018 | PLDI | Verifying that web pages have accessible layout. | Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil |
| 2018 | PLDI | Relay: a new IR for machine learning frameworks. | Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock |
| 2018 | PLDI | Finding root causes of floating point error. | Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock |
| 2016 | CAV | Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. | Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock |
| 2016 | CAV | 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 |
| 2016 | CPP | 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 |
| 2016 | OOPSLA | Scalable verification of border gateway protocol configurations with an SMT solver. | Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock |
| 2016 | PLDI | Verified peephole optimizations for CompCert. | Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman |
| 2015 | HRI | Visual Robot Programming for Generalizable Mobile Manipulation Tasks. | Sonya Alexandrova, Zachary Tatlock, Maya Cakmak |
| 2015 | ICRA | RoboFlow: A flow-based visual programming language for mobile manipulation tasks. | Sonya Alexandrova, Zachary Tatlock, Maya Cakmak |
| 2015 | PLDI | Automatically improving accuracy for floating point expressions. | Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock |
| 2015 | PLDI | 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 |
| 2014 | NDSS | SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks. | Dongseok Jang, Zachary Tatlock, Sorin Lerner |
| 2014 | OSDI | Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. | Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock |
| 2014 | PLDI | Automating formal proofs for reactive systems. | Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner |
| 2010 | PLDI | Bringing extensibility to verified compilers. | Zachary Tatlock, Sorin Lerner |
| 2009 | PLDI | Proving optimizations correct using parameterized program equivalence. | Sudipta Kundu, Zachary Tatlock, Sorin Lerner |
| 2009 | POPL | Equality saturation: a new approach to optimization. | Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner |
| 2008 | OOPSLA | Deep typechecking and refactoring. | Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner |