PV2 SynPlexitysynthesises recursive functions that satisfy a functional specification and an asymptotic resource bound

Synthesis tool for recursive functions that satisfy both a functional specification and an asymptotic resource bound. Example usage: User asks the tool to synthesize an implementation of a sorting function with resource usage O(n log n) where n is the length of the input list.

Application domain/field

Type of tool

Synthesis tool

Expected input


.sq file?


Implemented on top of Synquid, uses Z3. It uses a type-directed synthesis algorithm.


License: MIT license


Repository: https://github.com/Herbping/Synplexity

Related papers

Synthesis with Asymptotic Resource Bounds (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: Synquid and ReSyn

ProVerB specific

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