Example-Driven Recursive Program Synthesis
This repository contains the source code of this thesis Oracle-free Synthesis of Recursive Programs.
The codebase implements two algorithms: TypedEscher and AscendRec
TypedEscher is a Scala implementation of the Escher algorithm, described in this paper Recursive Program Synthesis(CAV'13), with the addition of a polymorphic static type system and other type-related optimizations to improve searching efficiency.
AscendRec is a new algorithm based on TypedEscher, but unlike TypedEscher, which requires the user to provide additional input-output examples during synthesis, AscendRec dose not need any additional examples to work.
Simply download or clone this project and run sbt from within the root directory.
To compile and run the benchmark suits, use sbt run and choose RunTypedEscher or RunAscendRec as the Main Class.
Results taken from the thesis.
See full output logs in result_TypedEscher.txt and result_AscendRec.txt
- Duplicate each element of a list
- Cartesian product of two lists
- Square of naturals
- Remove adjacent duplicates in a list
- Remove all duplicates in a list (synthesized without using additional components)
