Skip to main content

A simple inductive synthesis methodology and its applications

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv

DOI 10.1145/1869459.1869463 dblp BibTeX

Abstract

Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology for inductive synthesis that allows us to do this.

Related papers

FlashMeta: a framework for inductive program synthesis OOPSLA 2015
An inductive synthesis framework for verifiable reinforcement learning PLDI 2019
Model-guided synthesis of inductive lemmas for FOL with least fixpoints OOPSLA 2022
A Methodology for Lisp Program Construction from Examples POPL 1976
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants TACAS 2023
Recursive proofs for inductive tree data-structures POPL 2012
Semantic programming by example with pre-trained models OOPSLA 2021
A Methodology for Synthesis of Recursive Functional Programs TOPLAS 1987