Formal verification of approximate-DP via the characteristic function

Undergraduate Honor Thesis

Introduced an imperative language along with a novel type system that helps developers in writing algorithms that satisfy differential privacy. The type system converts the probablistic program into a deterministic one, thus making it verifiable via off-the-shelf verifier. I verified the verifiable deterministic algorithms using model checker CPAChecker. I also proved the soundness of the type system, and showed an example algorithm (along with it’s verified version) using my language.

I presented this work at ACM conference on Programming Language Design and Implementation (PLDI’23)’s student research competition, where I was selected as one of the finalist.