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

Format:

.sq file?

Internals

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

Comments

License: MIT license
Synthesis

Links

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

Last commit date

27 May 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_37 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: Synquid and ReSyn

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.