Projects
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.
Publications
Past events
- OOPSLA 2022: External Review / Artifact Evaluation Committee member
- VMCAI 2022: Artifact Evaluation Committee member
- Attended Markoberdorf Summer School 2018
- Participated in Dagstuhl Seminar 18111 on Loop Optimization
- PLDI 2018: Artifact Evaluation Committee member
TAships
CSC410 - Fall 2021: Software Verification and Testing | |
Project: Toy Synthesizer | |
CSC410 - Fall 2020: Software Verification and Testing | |
SAT solving with z3 | |
SMT solving with z3 | |
Program synthesis with Rosette | |
CSC410 - Fall 2019: Software Verification and Testing | |
Tutorial 2: SAT solving with z3 | |
CSC410 - Fall 2017: Software Verification and Testing | |
Tutorial 1: z3 | |
Tutorial 2: PyCParser and visiting AST nodes | |
Tutorial 3: Short introduction to Rosette | |
Projects 1-5 resources | |
CSC324: Programming Languages |