Current Projects
Fast and flexible e-graphs for optimization, synthesis, and verification
Automatically inferring rewrite rules by and for equality saturation
Numerical benchmarks, tools, and standards
Automatically improving numerical accuracy
Synthesizing and optimizing carpentry build plans
PL tools and techniques for 3D printing
Past Projects
Functional compiler IR for machine learning
Formally verified, accurate fast-math optimizations
Number system design tools
Building and maintaining large verification efforts
Correctly compile Coq in Coq via CompCert
Modular verification of distributed systems
Automated reasoning for web page layout
Dynamic binary analysis for numerical error
Verifying safety of radiotherapy controls at CNTS
Verifying distributed systems implementations
Formally verified solver-aided tools
Formal verification for BGP router configurations
Extensible, formally verified peephole optimization framework for CompCert
Visual robot programming framework
Formally verified BPF JIT compiler for Linux via CompCert
Formally verified reactive programming framework for system shims
Compiler-enforced VTable hijacking defenses
Formally verified web browser kernel
Emergent loop optimizations via equality saturation and PEGs
Extensible, formally verified optimizations via parameterized translation validation
Deep typechecking and refactoring for embedded DB queries in Java