Recursive Program Synthesis - Aws Albarghouthi

Aws Albarghouthi, Associate Professor of Computer Science at the University of Wisconsin-Madison, discusses his paper “Recursive Program Synthesis”, which introduced Escher, an inductive synthesis algorithm for learning recursive programs from input-output examples.

The project emerged from Albarghouthi’s early work in program verification and inductive proofs for recursive procedures. After he and fellow graduate student Zachary Kincaid developed initial ideas for synthesizing recursive programs, they cold-emailed Sumit Gulwani at Microsoft Research, whose feedback and collaboration helped shape the direction of the paper.

In This Episode -

• Recursive synthesis from examples

• Escher’s forward and backward search

• Goal graphs for partial programs

• Components as reusable building blocks

• Synthesis benchmarks and comparisons with Sketch

• Quantum compiler synthesis

• Qubit mapping and routing synthesis- Agent correctness and prompt injection

References -

• Microsoft PROSE: https://www.microsoft.com/en-us/research/project/prose/

• SKETCH: https://people.csail.mit.edu/asolar/papers/Solar-Lezama09.pdf

• Generating Compilers for Qubit Mapping and Routing: https://arxiv.org/abs/2508.10781

• Synthesizing Quantum-Circuit Optimizers: https://arxiv.org/abs/2211.09691

• 'Introduction to Neural Network Verification' book: https://verifieddeeplearning.com/

About the Paper -

“Recursive Program Synthesis”

Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid

Computer Aided Verification, CAV 2013The paper presents Escher, a synthesis algorithm that learns recursive procedures from input-output examples. Escher combines component-based enumeration, interactive example refinement, and a goal graph that helps assemble partial programs into complete recursive solutions.

https://www.microsoft.com/en-us/research/publication/recursive-program-synthesis/

About the Guest -

Aws Albarghouthi is an associate professor of computer science at the University of Wisconsin-Madison. His research focuses on program synthesis, formal verification, quantum computing systems, and the correctness of AI agents.

https://pages.cs.wisc.edu/~aws/

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com