Synthesizing Imperative Programs from Examples Guided by Static Analysis

TL;DR

This paper introduces SIMPL, a static analysis-guided program synthesis algorithm that efficiently generates complete imperative programs from examples, significantly reducing search space and solving introductory programming problems quickly.

Contribution

The paper presents a novel static analysis-guided synthesis algorithm that combines enumeration with pruning to efficiently generate correct programs from examples.

Findings

Solved 30 benchmark problems in 6.6 seconds on average

Effective pruning reduces search space significantly

First to integrate static analysis with enumerative synthesis for this task

Abstract

We present a novel algorithm that synthesizes imperative programs for introductory programming courses. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our key idea is to combine enumerative program synthesis and static analysis, which aggressively prunes out a large search space while guaranteeing to find, if any, a correct solution. We have implemented our algorithm in a tool, called SIMPL, and evaluated it on 30 problems used in introductory programming courses. The results show that SIMPL is able to solve the benchmark problems in 6.6 seconds on average.