Research & engineering
My work focuses on program verification, formal methods, and automata theory. Below are selected research and engineering projects from my doctoral work, publications, internships, and research positions.
This project investigates the relationship between Markov Decision Processes and probabilistic powerdomains. It leverages this theoretical development to offer a fast symbolic optimal synthesis engine for McNetKAT programs. THe manuscript is currently in preparation for PLDI 2027.
This ongoing project investigates completeness for control-flow extensions of Guarded Kleene Algebra with Tests. The manuscript is currently in preparation for PLDI 2027.
This project studies Weighted Guarded Kleene Algebra with Tests (GKAT), extending algebraic tools for program reasoning to quantitative settings. The work develops completeness and complexity results for the weighted system and was presented at the International Colloquium on Automata, Languages, and Programming (ICALP) in 2025.
Paper →I designed, built, and tested a compiler written in TypeScript for translating legacy programs written in a complex policy-as-code source language into a streamlined domain-specific language. This work combined programming language design, compiler engineering, and practical software testing.
I applied exponential control barrier functions to autonomous vehicle safety, including settings with high relative degree dynamics and unbounded uncertainty. The project involved designing and simulating safe controllers across traffic scenarios and led to a publication at the IEEE Intelligent Vehicles Symposium in 2022.
Paper →I developed frontend and backend features for Kindle e-readers and Kindle iOS and Android apps, including synchronization features, backend metrics, and features on the frontend home page on e-readers.
I worked as a genomics research assistant analyzing transcriptomes in R, gaining experience with computational biology workflows and data analysis.