Headshot of Zachary, a smiling man with glasses, curly black hair, and a beard.

Zachary J. Susag

PhD student, PL @ Cornell


I am a PhD student in the Department of Computer Science at Cornell University and a proud member of the PL @ Cornell research group. At Cornell, I research programming languages and applied formal methods under the advisement of Prof. Justin Hsu. Most recently, I’ve been working on Plinko: a symbolic execution technique for verifying properties of randomized programs.

Before arriving at Cornell, I was a PhD student at the University of Wisconsin–Madison. While working on my undergraduate degree at Grinnell College, I worked with Prof. Peter-Michael Osera on type-and-example driven program synthesis, and Prof. Claire Le-Goues and Prof. Ruben Martins at Carnegie Mellon University as part of the REUSE REU program during the summer of 2018.

Research interests

I design and develop tools to formally verify the correctness of programs, especially those that use randomization. Programming is nuanced and error-prone. Probabilistic programming only exacerbates these traits, requiring practitioners to also juggle the subtlety of probabilistic reasoning. Differential privacy is a prime example of a class of randomized algorithms that have been proven to be exceptionally difficult to correctly write. Through my research I hope to make it easier for people to harness computing in a safe, verifiable manner.


I’m going to be presenting “Symbolic Execution for Randomized Programs” in-person at OOPSLA 2022 in Auckland, New Zealand.
My website is live!
“Symbolic Execution for Randomized Programs” has been accepted to OOPSLA 2022.


  1. Symbolic Execution for Randomized Programs
    Proceedings of the ACM on Programming Languages