Hi ! I am a PhD student 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.



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.


Modular Divide-And-Conquer Paralellization of Nested Loops pdf ext
Synthesis of Divide and Conquer Parallelism for Loops pdf

Past events