Projects

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

Œuf
Correctly Compile Coq in Coq via CompCert

Distributed Components
Modular Verification of Distributed Systems

Cassius
Automated Reasoning for Webpage Layout

Herbgrind
Dynamic Binary Analysis for Numerical Error

Neutrons
Verifying Safety for Radiotherapy Control
CNTS  

Verdi
Verifying Distributed Systems Implementations