Research Projects
PTX Kernel Equivalence Checker
Building a PTX-level equivalence checker that uses symbolic execution to formally verify whether optimized GPU kernels—generated by LLMs or handwritten by compiler experts—preserve the semantics of their unoptimized counterparts. This work advances trustworthy AI-assisted codegen by enabling functional equivalence checking at the assembly level.
LLM-Vectorizer: LLM-based Verified Loop Vectorizer
Developed a framework that prompts large language models (LLMs) to rewrite scalar loops into vectorized form, and then formally verifies the transformation using SMT solvers.
Accera: Compiler to accelerate AI workloads
Contributed to Accera, a domain-specific compiler designed to optimize compute-intensive algorithms for both CPU and GPU targets. The system lowers a Python-based scheduling DSL to MLIR, where a series of transformations and lowerings are applied before generating LLVM IR and machine code. I extended the DSL with features to express loop scheduling optimizations and implemented custom transformations across the MLIR and LLVM IR stages to enable high-performance code generation for diverse hardware backends.
Dissertation: Improving Compiler Construction Using Formal Methods
This dissertation focuses on improving compiler reliability and performance using formal methods, particularly in the context of LLVM. As programming languages become more high-level and processors more specialized, compilers must effectively bridge the growing gap between the two. The core contribution is the development of precise and sound static analyses using SMT solvers to identify code properties essential for optimizations like dead code elimination.
Testing LLVM’s Static Analyses for Precision and Soundness
Developed a framework that uses SMT solvers to test the precision and soundness of static analyses in production compilers like LLVM. The system generates ground truth analysis results offline—too slow for production use but ideal for validating existing compiler analyses. This approach helped uncover numerous precision issues and rediscovered previously fixed soundness bugs that had regressed. The work bridges formal methods with practical compiler development, enabling more trustworthy and optimizable code.
Souper: Superoptimizer for LLVM IR
Souper is a synthesis-based superoptimizer for LLVM IR that automatically discovers optimal, verified peephole optimizations using SMT solvers. It encodes code fragments as logical formulas, searches for equivalent but more efficient replacements, and guarantees correctness through formal verification. The project advances compiler automation by improving optimization quality beyond what is hand-written in LLVM.
Automatic Generation of a PeepHole Optimizer
Worked on using the superoptimization technique to automatically generate a peephole optimizer for the Cranelift JIT compiler, which compiles WebAssembly to machine code for x86 and ARM target architecture. Mentor: Nick Fitzgerald and Dan Gohman.