Projects

Using local, or intrinsic, definitions of data structures to develop predictable verification for data structures and systems.

Using approximate solvers for non-linear real arithmetic to improve differential privacy verification.

An error-bounded lossy compressor for scientific datasets on GPUs.

A set of algorithms for multiplying irregularly-shaped matrices fast on GPUs.