Hi ! I am fifth year PhD candidate in the Software Engineering Group at the University of Toronto. I am mostly interested in formal methods and program synthesis, with a particular focus on parallel programs.
My advisor is Azadeh Farzan.



Synduce synthesizes recursive functions given a functional specification. In the background, it takes advantage of selective bounding techniques to solve non-trivial problems, efficiently utilizing off-the-shelf solvers for finding solutions to recursion-free abstractions of the original problem.


Parsynt is a tool designed to synthesize a divide-and-conquer style implementation of a given loop, along with a proof that this implementation is equivalent to the one provided as input. We currently take as input a C program with for loops and output a parallel version written in C++ using Intel's Threading Building Blocks [TBB] library. The proof verifying that this implementation is equivalent to the sequential one given as input is encoded in Dafny, a language and program verifier for functional correctness.


Recursion Synthesis with Unrealizability Witnesses
PLDI 2022 with and Danya Lette
Counterexample-Guided Partial Bounding for Recursive Function Synthesis extended
Phased Synthesis of Divide-And-Conquer Programs full
Modular Divide-And-Conquer Parallelization of Nested Loops extended
Synthesis of Divide and Conquer Parallelism for Loops

Past events


From Iterative Implementations to Single Pass Functions