Synquid generates programs from concise, high-level type-based specifications. It's the first synthesizer to automatically discover provably correct implementations of sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. For these programs, the required specifications are up to seven times more concise than the implementations, and the synthesis times range from fractions of a second (for insertion sort) to under a minute (for Red-Black Tree rotations)
If you would like to contact us about our work, please scroll down to the people section and click on one of the group leads' people pages, where you can reach out to them directly.