Reconciling enumerative and deductive program synthesis
Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, Yanjun Wang
Abstract
Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability.
Topics & Concepts
CorrectnessComputer scienceProgram synthesisProgramming languageScalabilityConstruct (python library)SyntaxImplementationDeductive databaseTheoretical computer scienceArtificial intelligenceDatabaseSoftware Engineering ResearchLogic, programming, and type systemsSoftware Testing and Debugging Techniques