Programming Languages and Formal Methods

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.