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.
|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|