research
Formal Methods, Machine Learning for Systems, and High-Performance Computing.
Code-aware Neural Surrogates for HPC Applications
Combines machine learning with program analysis and compiler optimizations to accelerate performance-critical kernels in large-scale HPC codes.
Scaling Floating-Point Error Tracking with Whole-Program Shadow Execution
Tracks floating-point error across optimized HPC applications using LLVM instrumentation and higher-precision shadow execution, including multi-module and MPI workloads.
Verifying Exact Conditions for Implementations of Density Functional Approximations
An automated formal verification pipeline that proves simulation code satisfies its required physical constraints, or produces concrete counterexamples where it does not.