Zachary Tatlock / Research

My primary goal is to help my students become great researchers. That means working with them as they practice developing their own research questions and learning how to get unstuck as we answer those questions.

Consequently, our “research portfolio” is diverse. We’ve worked on:

Formally verifying distributed systems implementations in proof assistants
Automatically rewriting code to minimize rounding error
Decompiling triangle meshes back to more-editable 3D CAD designs
Building new proof assistants to reason about accessiblity in web browsers
Automatically trading off time and space in GPU memory for ML training
Formally verifying controls in an active clinical radiotherapy installation
Using SMT to scale proof assistant based verification of BGP router configs

Current Projects

egg: Fast and flexible e-graphs for optimization, synthesis, and verification
Lakeroad: FPGA technology mapping via enumerative program synthesis
Optimizations to enable illusion knitting on CNC knitting machines
Sparse autodiff for second-order optimization and simulation methods
Ruler: Automatically inferring rewrite rules by and for equality saturation
Herbie: Automatically improving numerical accuracy
FPBench: Numerical benchmarks, tools, and standards

Past Projects

Carpentry Compiler: Synthesizing and optimizing carpentry build plans
Glenside: Term rewriting for flexible tensor operator mapping
Incarnate: PL tools and techniques for 3D printing
TVM Relay: Functional compiler IR for machine learning
Icing: Formally verified, accurate fast-math optimizations
Titanic: Number system design tools
Proof Engineering: Building and maintaining large verification efforts
Œuf: Correctly compile Coq in Coq via CompCert
Distributed Components: Modular verification of distributed systems
Cassius: Automated reasoning for web page layout
Herbgrind: Dynamic binary analysis for numerical error
Neutrons: Verifying safety of radiotherapy controls at CNTS
Verdi: Verifying distributed systems implementations
SpaceSearch: Formally verified solver-aided tools
Bagpipe: Formal verification for BGP router configurations
Peek: Extensible, formally verified peephole optimization framework for CompCert
Roboflow: Visual robot programming framework
Jitk: Formally verified BPF JIT compiler for Linux via CompCert
Reflex: Formally verified reactive programming framework for system shims
SafeDispatch: Compiler-enforced VTable hijacking defenses
Quark: Formally verified web browser kernel
Peggy: Emergent loop optimizations via equality saturation and PEGs
PEC/XCert: Extensible, formally verified optimizations via parameterized translation validation
Quail: Deep typechecking and refactoring for embedded DB queries in Java

Please see our publications for more.