Incarnate
PL Tools and Techniques for 3D Printing
egg
Fast and Flexible E-graphs for Synthesis
TVM Relay
Functional Compiler IR for Machine Learning
Titanic
Floating-Point Number System Design Tools
FPBench
Numerical Benchmarks, Compilers, Standards
Carpentry Compiler
Synthesize and Optimize Carpentry Build Plans
Icing
Accurate, Formally Verified Fast-math Optimizations
Herbie
Automatically Improving Numerical Accuracy
Proof Engineering
Building and Maintaining Systems in Proof Assistants
Distributed Components
Modular Verification of Distributed Systems
Cassius
Automated Reasoning for Webpage Layout
Herbgrind
Dynamic Binary Analysis for Numerical Error
Verdi
Verifying Distributed Systems Implementations
Checking out past projects can also help provide a sense for the sort of work we do: