Zachary J. Susag
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.
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.