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

Zachary J. Susag

PhD student, PL @ Cornell

About

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.

News

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

Publications

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