PV2 Synducegenerates equivalent recursive functions when migrating from one data structure to another

Application domain/field

Type of tool

Synthesis tool

Expected input


One of the following:

Expected output

Recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton.


The context that they consider is one where you have two data types A and B. You have implemented a recursive function for A, and now want to implement this for B. Synduce uses bounded model checking to check the validity of a synthesis solution. Uses Z3 and CVC4.


License: MIT
Model checking OCaml Synthesis


Repository: https://github.com/synduce/Synduce

Related papers

Counterexample-Guided Partial Bounding for Recursive Function Synthesis (CAV '21)

Last publication date

15 July 2021

Related tools

Tools for synthesizing recursive functional programs: Escher, λ2, Myth, Myth2, SynQuid, SyntRec, Leon.

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.