Synthesizing Imperative Programs for Introductory Programming Assignments
Hakjoo Oh
Korea University
hakjoo oh@korea.ac.kr

arXiv:1702.06334v2 [] 13 Jun 2017

Sunbeom So
Korea University
sunbeom so@korea.ac.kr

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 S IMPL,
and evaluated it on 30 problems used in introductory programming courses. The results show that
S IMPL is able to solve the benchmark problems in
6.6 seconds on average.

1 Introduction
Our long-term goal is to build an intelligent tutoring system that helps students to improve their programming skills.
Our experience in introductory programming courses is that
students, who learn programming for the first time, often
struggle with solving programming problems for themselves.
Manually providing guidance simply does not scale for the increasingly large number of students. To make matters worse,
we found that even instructors sometimes make mistake and
shy students are reluctant to ask questions. Motivated by this
experience, we aim to build an automatic system that helps
students to improve their skills without human teachers.
In this paper, we present a key component of the system,
which automatically generates complete programs from students’ incomplete programs. The inputs of the algorithm
are a partial program with constraints on variables and constants, and input-output examples that specify the program’s
behavior. The output is a complete program whose behavior
matches all of the given input-output examples.
The key novelty of our algorithm is to combine enumerative program synthesis and program analysis techniques. It
basically enumerates every possible candidate program in increasing size until it finds a solution. This algorithm, however, is too slow to be interactively used with students due
to the huge search space of programs. Our key idea to accelerate the speed is to perform static analysis alongside the
enumerative search, in order to “statically” identify and prune

out interim programs that eventually fail to be a solution. We
formalize our pruning technique and its safety property.
The experimental results show that our algorithm is remarkably effective to synthesize introductory imperative programs. We have implemented the algorithm in a tool, S IMPL,
and evaluated its performance on 30 programming tasks used
in introductory courses. With our pruning technique, S IMPL
is fast enough to solve each problem in 6.6 seconds on average. However, without the pruning, the baseline algorithm,
which already adopts well-known optimization techniques,
takes 165.5 seconds (25x slowdown) on average.
We summarize our contributions below:
• We present a new algorithm for synthesizing imperative
programs from examples. To our knowledge, our work
is the first to combine enumerative program synthesis
and static analysis technologies.
• We prove the effectiveness of our algorithm on 30 real
programming problems used in introductory courses.
The results show that our algorithm quickly solves the
problems, including ones that most beginner-level students have hard times to solve.
• We provide a tool, S IMPL , which is publicly available
and open-sourced.1

2 Showcase
In this section, we showcase S IMPL with four programming
problems that most beginners feel difficult to solve. To use
S IMPL, students need to provide (1) a partial program, (2) a
set of input-output examples, and (3) resources that S IMPL
can use. The resources consist of a set of integers, a set of
integer-type variables, and a set of array-type variables. The
goal of S IMPL is to complete the partial program w.r.t. the
input-output examples, using only the given resources.
Problem 1 (Reversing integer) The first problem is to
write a function that reverses a given integer. For example,
given integer 12, the function should return 21. Suppose a
partial program is given as
reverse (n){ r := 0; while(?){?}; return r;}
1

Hidden for double-blind reviewing.

reverse(n){
r := 0;
while ( n > 0 ){
x := n % 10;
r := r * 10;
r := r + x;
n := n / 10;
};
return r;
}

(a) Problem1
sum(n){
r := 0;
while ( n > 0 ){
t := n;
while (t > 0){
r := r + t;
t := t - 1;
};
n := n - 1;
};
return r;
}

(c) Problem 3

count(n,a){
while ( n > 0 ){
t := n % 10;
a[t] := a[t] + 1;
n := n / 10;
};
return a;
}

(b) Problem 2
abssum(a, len){
r := 0;
i := 0;
while (i < len){
if ( a[i] < 0 )
{ r := r - a[i]; }
else
{ r := r + a[i]; }
i := i + 1;
};
return r;
}

(d) Problem 4

Figure 1: Synthesized results by S IMPL (in the boxes)
where ? denotes holes that need to be completed. Suppose
further S IMPL is provided with input-output examples {1 7→
1, 12 7→ 21, 123 7→ 321}, integers {0, 1, 10}, and integer
variables {n, r, x}.
Given this problem, S IMPL produces the solution in Figure 1(a) in 2.5 seconds. Note that, S IMPL finds out that the
integer ‘1’ is unnecessary and the final program does not contain it. Also, S IMPL does not require sophisticated examples,
so that S IMPL can be easily used by inexperienced students.
Problem 2 (Counting) The next problem is to write a function that counts the number of each digit in an integer. The
program takes an integer and an array as inputs, where each
element of the array is initially 0. As output, the program returns that array but now each array element at index i stores
the number of is that occur in the given integer. For example, when a tuple (220, h0, 0, 0i) is given, the function should
output h1, 0, 2i; 0 occurs once, 1 does not occur, and 2 occurs
twice in ‘220’. Suppose the partial program is given as
count(n,a){ while(?){?}; return a;}

with examples {(11, h0, 0i) 7→ h0, 2i, (220, h0, 0, 0i) 7→
h1, 0, 2i}, integers {0, 1, 10}, integer variables {i, n, t}, and
an array variable {a}.
For this problem, S IMPL produces the program in Figure 1(b) in 0.2 seconds. Note that S IMPL uses a minimal set
of resources; i is not used though it is given as usable.
Problem 3 (Sum of sum) The third problem is to compute
1 + (1 + 2) + ... + (1 + 2 + ... + n) for a given integer n.
Suppose the partial program

sum(n){ r := 0; while(?){?}; return r;}

is given with examples {1 7→ 1, 2 7→ 4, 3 7→ 10, 4 7→ 20},
integers {0, 1}, and integer-type variables {n, t, r}.
Then, S IMPL produces the program in Figure 1(c) in 37.6
seconds. Note that S IMPL newly introduced a nested loop,
which is absent in the partial program.
Problem 4 (Absolute sum) The last problem is to sum the
absolute values of all the elements in a given array. We provide the partial program:
abssum(a, len){ r := 0; i := 0;
while(i < len){ if(?){?} else{?}; i:=i+1;};
return r;}

where the goal is to complete the condition and bodies
of the if-statement. Given a set of input-output examples
{(h−1, −2i, 2) 7→ 3, (h2, 3, −4i, 3) 7→ 9}, an integer {0},
integer variables {r, i}, and an array variable {a}, S IMPL
produces the program in Figure 1(d) in 12.1 seconds.

3 Problem Definition
Language We designed an imperative language that is small
yet expressive enough to deal with various programming
problems in introductory courses. The syntax of the language
is defined by the following grammar:
⊕ → + | − | ∗ | / | %, ≺→ =|>|<
l → x | x[y], a → n | l | l1 ⊕ l2 | l ⊕ n | ♦
b → true | false | l1 ≺ l2 | l ≺ n | b1 ∧ b2 | b1 ∨ b2 | ¬b | △
c → l := a | skip | c1 ; c2 | if b c1 c2 | while b c | 

An l-value (l) is a variable (x) or an array reference (x[y]).
An arithmetic expression (a) is an integer constant (n), an
l-value (l), or a binary operation (⊕). A boolean expression
(b) is a boolean constant (true, false), a binary relation (≺),
a negation (¬b), or a logical conjunction (∧) and disjunction
(∨). Commands include assignment (l := a), skip (skip), sequence (c1 ; c2 ), conditional statement (if b c1 c2 ), and whileloop (while b c).
A program P = (x, c, y) is a command with input and output variables, where x is the input variable, c is the command,
and y is the output variable. The input and output variables x
and y can be either of integer or array types. For presentation
brevity, we assume that the program takes a single input, but
our implementation supports multiple input variables as well.
An unusual feature of the language is that it allows to write
incomplete programs. Whenever uncertain, any arithmetic
expressions, boolean expressions, and commands can be left
out with holes (♦, △, ). The goal of our synthesis algorithm
is to automatically complete such partial programs.
The semantics of the language is defined for programs
without holes. Let X be the set of program variables, which
is partitioned into integer and array types, i.e., X = Xi ⊎ Xa .
A memory state
m ∈ M = X → V,

v ∈ V = Z + Z∗

is a partial function from variables to values (V). A value
is either an integer or an array of integers. An array a ∈
Z∗ is a sequence of integers. For instance, we write h1, 2, 3i

A[[n]](m) = n
A[[x]](m) = m(x)
A[[x[y]]](m) = m(x)m(y)
A[[l1 ⊕ l2 ]](m) = A[[l1 ]](m) ⊕ A[[l2 ]](m)
A[[l ⊕ n]](m) = A[[l]](m) ⊕ n
B[[true ]](m) = true
B[[false]](m) = false
B[[l1 ≺ l2 ]](m) = A[[l1 ]](m) ≺ A[[l2 ]](m)
B[[l ≺ n]](m) = A[[l]](m) ≺ n
B[[b1 ∧ b2 ]](m) = B[[b1 ]](m) ∧ B[[b2 ]](m)
B[[b1 ∨ b2 ]](m) = B[[b1 ]](m) ∨ B[[b2 ]](m)
B[[¬b]](m) = ¬B[[b]](m)
C[[x := a]](m) = m[x 7→ A[[a]](m)]
A[[a]](m)
C[[x[y] := a]](m) = m[x 7→ m(x)m(y) ]
C[[skip]](m) = m
C[[c1 ; c2 ]](m) = (C[[c2 ]] ◦ C[[c1 ]])(m)
C[[if b c1 c2 ]](m) = cond(B[[b]], C[[c1 ]], C[[c2 ]])(m)
C[[while b c]](m) = (fix F )(m)
where F (g) = cond(B[[b]],
g ◦ C[[c]], λx.x)

f (m) if p(m) = true
cond(p, f, g)(m) =
g(m) if p(m) = false

Figure 2: Semantics of the language
for the array of integers 1, 2, and 3. We write |a|, ai , and
aki for the length of a, the element at index i, and the array
a0 . . . ai−1 kai+1 . . . a|a|−1 , respectively.
The semantics of the language is defined by the functions:
A[[a]] : M → V, B[[b]] : M → B, C[[c]] : M → M
where A[[a]], B[[b]], and C[[c]] denote the semantics of arithmetic expressions, boolean expressions, and commands, respectively. Figure 2 presents the denotational semantics,
where fix is a fixed point operator. Note that the semantics
for holes is undefined.
Synthesis Problem A synthesis task is defined by the five
components:
((x, c, y), E, Γ, Xi , Xa )
where (x, c, y) is an incomplete program with holes, E ⊆
V × V is a set of input-output examples. Γ ⊆ Z is a set of
integers, Xi is a set of integer-type variables, and Xa is a set
of array-type variables. The goal of our synthesis algorithm
is to produce a complete command c without holes such that
• c uses constants and variables in Γ and Xi ∪ Xa , and
• c is consistent with every input-output example:

∀(vi , vo ) ∈ E. C[[c]]([x 7→ vi ]) (y) = vo .

4 Synthesis Algorithm
In this section, we present our synthesis algorithm that combines enumerative search with static analysis.

4.1

Synthesis as State-Search

We first reduce the synthesis task into a state-search problem.
Consider a synthesis task ((x, c, y), E, Γ, Xi , Xa ). The corresponding search problem is defined by the transition system
(S, →, s0 , F ) where S is a set of states, (→) ⊆ S × S is a
transition relation, s0 ∈ S is an initial state, and F ⊆ S is a
set of solution states.

Algorithm 1 Synthesis Algorithm
Input: A synthesis problem ((x, c0 , r), E, Γ, Xi , Xa )
Output: A complete program consistent with E
1: W ← {c0 }
2: repeat
3:
Pick the smallest state s from W
4:
if s is a terminal state then
5:
if solution(s) then return s
6:
else
7:
if ¬prune(s) then W ← W ∪ next(s)
8: until W 6= ∅
• States : A state s ∈ S is a command possibly with holes,
which is defined by the grammar in Section 3.
• Initial state : An initial state s0 is a partial command c0 .
• Transition relation : Transition relation (→) ⊆ S × S
determines the state that is immediately reachable from a
state. The relation is defined as a set of inference rules in
Figure 3. Intuitively, a hole can be replaced by an arbitrary expression (or command) of the same type. Given
a state s, we write next(s) for the set of all immediate
next states, i.e., next(s) = {s′ | s → s′ }. We write s 6→
for terminal states, i.e., states with no holes.
• Solution states : A state s is a solution iff s is a terminal
state and it is consistent with all input-output examples:
solution(s) ⇐⇒

s 6→ ∧ ∀(vi , vo ) ∈ E. C[[s]]([x 7→ vi ]) (y) = vo .

4.2

Baseline Search Algorithm

Algorithm 1 shows the basic architecture of our enumerative
search algorithm. The algorithm initializes the workset W
with c0 (line 1). Then, it picks a state s with the smallest
size and removes the state from the workset (line 3). If s is
a solution state, the algorithm terminates and s is returned
(line 5). For a non-terminal state, the algorithm attempts to
prune the state by invoking the function prune (line 7). If
pruning fails, the next states of s are added into the workset
and the loop repeats. The details of our pruning technique
is described in Section 4.3. At the moment, assume prune
always fails.
The baseline algorithm implicitly performs two wellknown optimization techniques. First, it maintains previously
explored states and never reconsider them. Second, more importantly, it normalizes states so that semantically-equivalent
programs are also syntactically the same. For instance, suppose (r := 0; r := x ∗ 0; ) is the current state. Before
pushing it to the workset, we first normalize it to (r := 0; ).
To do so, we use four code optimization techniques: constant
propagation, copy propagation, dead code elimination, and
expression simplification [Aho et al., 1986]. These two techniques significantly improve the speed of enumerative search.
In addition, the algorithm considers terminating programs
only. Our language has unrestricted loops, so the basic algorithm may synthesize non-terminating programs. To exclude
them from the search space, we use syntactic heuristics to detect potentially non-terminating loops. The heuristics are: 1)

c1 → c′1
c2 → c′2
c1 → c′1
c2 → c′2
b → b b′
b → b b′
a →a a ′
′
′
′
′
′
′
l := a → l := a c1 ; c2 → c1 ; c2 c1 ; c2 → c1 ; c2 if b c1 c2 → if b c1 c2 if b c1 c2 → if b c1 c2 if b c1 c2 → if b c1 c2 ¬b →b ¬b′
b1 →b b′1
b2 →b b′2
b2 →b b′2
b1 →b b′1
b → b b′
c → c′
while b c → while b′ c while b c → while b c′ b1 ∧ b2 →b b′1 ∧ b2 b1 ∧ b2 →b b1 ∧ b′2 b1 ∨ b2 →b b′1 ∨ b2 b1 ∨ b2 →b b1 ∨ b′2
 → l := ♦  → skip
△ →b l ≺ n

 → ; 

△ →b △ ∧ △

 → if △  

△ →b △ ∨ △

 → while △ 

△ →b ¬△

♦ →a n

△ →b true △ →b f alse △ →b l1 ≺ l2
♦ →a l

♦ → a l1 ⊕ l2

♦ →a l ⊕ n

Figure 3: Transition Relation (n ∈ Γ, l ∈ Xi ∪ {x[y] | x ∈ Xa ∧ y ∈ Xi })

example1(n){
r := 0;
while (n > 0){
r := n + 1;
n := ♦;
};
return r;
}

example2(n) {
r := 0;
while (n > 0){
;
r := x * 10;
n := n / 10;
};
return r;
}

(a)

(b)

Figure 4: States that are pruned away
we only allow boolean expressions of the form x < y (or
x > n) in loop conditions, 2) the last statement of the loop
body must increase (or decrease) the induction variable x, and
3) x and y are not defined elsewhere in the loop.

4.3

Pruning with Static Analysis

Now we present the main contribution of this paper, pruning
with static analysis. Static analysis allows to safely identify
states that eventually fail to be a solution. We first define the
notion of failure states.
Definition 1. A state s is a failure state, denoted fail(s), iff
every terminal state s′ reachable from s is not a solution, i.e.,
fail(s) ⇐⇒ ((s →∗ s′ ) ∧ s′ 6→ =⇒ ¬solution(s′ )).
Our goal is to detect as many failure states as possible. We
observed two typical cases of failure states that often show up
during the baseline search algorithm.
Example 1. Consider the program in Figure 4(a) and inputoutput example (1, 1). When the program is executed with
n = 1, no matter how the hole (♦) gets instantiated, the output value r is no less than 2 at the return statement. Therefore, the program cannot but fail to satisfy the example (1, 1).
Example 2. Consider the program in Figure 4(b) and inputoutput example (1, 1). Here, we do not know the exact values
of x and r, but we know that 10 ∗ x = 1 must hold at the end
of the program. However, there exists no such integer x, and
we conclude the partial program is a failure state.
Static Analysis We designed a static analysis that aims to
effectively identify these two types of failure states. To do so,
our analysis combines numeric and symbolic analyses; the
numeric analysis is designed to detect the cases of Example 1

and the symbolic analysis for the cases of Example 2. The
abstract domain of the analysis is defined as follows:
b = X → V,
b
m
b ∈M

b =I×S
vb ∈ V

An abstract memory state m
b maps variables to abstract
b
values (V).
An abstract value is a pair of intervals (I)
and symbolic values (S). The domain of intervals is standard [Cousot and Cousot, 1977]:
I = ({⊥} ∪ {[l, u] | l, u ∈ Z ∪ {−∞, +∞} ∧ l ≤ u}, ⊑I).
For symbolic analysis, we define the following flat domain:
S = (SE⊤
⊥ , ⊑S ) where SE → n | βx (x ∈ Xi ) | SE ⊕ SE
A symbolic expression se ∈ SE is a constant (n), a symbol
(βx ), or a binary operation with symbolic expressions. We
introduce symbols one for each integer-type variable in the
program. The symbolic domain is flat and has the partial order: s1 ⊑S s2 ⇐⇒ (s1 = ⊥) ∨ (s1 = s2 ) ∨ (s2 = ⊤). We
b that transforms
define the abstraction function α : V → V
concrete values to abstract values:
α(n) = ([n, n], n)
α(n1 . . . nk ) = ([min{n1 , . . . , nk }, max{n1 , . . . , nk }], ⊤).
The abstract semantics is defined in Figure 5 by the functions:
b → V,
b
b
A[[a]]
:M

b → B,
b
b :M
B[[b]]

b →M
b
b :M
C[[c]]

b = {true,
[ ⊤ is the abstract boolean lattice.
d false}
where B
⊥
Intuitively, the abstract semantics over-approximates the
concrete semantics of all terminal states that are reachable
from the current state. This is done by defining the sound
b
b
b
semantics for holes: A[[♦]](
m),
b B[[△]](
m),
b and C[[]](
m).
b
An exception is that integer variables get assigned symbols,
rather than ⊤, in order to generate symbolic constraints on
integer variables.
In our analysis, array elements are abstracted into a single
b
b
element. Hence, the definitions of A[[x[y]]]
and C[[x[y]
:= a]]
do not involve y. Because an abstract array cell may represent
multiple concrete cells, arrays are weakly updated by joining
(⊔) old and new values. For example, in memory state m
b =
b
[x 7→ ([5, 5], ⊤), ...], C[[x[y]
:= 1]](m)
b evaluates to [x 7→
([1, 5], ⊤), ...].
For while-loops, the analysis performs a sound fixed point
computation. If the computation does not reach a fixed point
after a fixed number of iterations, we apply widening for

b
A[[n]](
m)
b
b m)
A[[l]](
b

=
=
=
=
=

b
B[[true
]](m)
b
b
B[[l1 ≺ l2 ]](m)
b
b ≺ n]](m)
B[[l
b
b
B[[b1 ∧ b2 ]](m)
b
b 1 ∨ b2 ]](m)
B[[b
b
b
B[[¬b]](
m)
b
b
B[[△]](
m)
b

=
=
=
=
=
=
=

b 1 ⊕ l2 ]](m)
A[[l
b
b ⊕ n]](m)
A[[l
b
b
A[[♦]](
m)
b

b := ♦]](m)
C[[x
b
b
C[[x[y] := ♦]](m)
b
b := a]](m)
C[[x
b
b
C[[x[y]
:= a]](m)
b
b
C[[skip]](
m)
b
b 1 ; c2 ]](m)
C[[c
b
b b c1 c2 ]](m)
C[[if
b
b
C[[while
b c]](m)
b
where Fb (g)

b
C[[]](
m)(x)
b

=
=
=
=
=
=
=
=
=
=

([n, n], n)
m(x)
b
(l = x or x[y])
b 1 ]](m)
b 2 ]](m)
b A[[l
A[[l
b ⊕
b
b
bn
A[[l1 ]](m)
b ⊕
([−∞, +∞], ⊤)
b
[
d (B[[false]](
true
m)
b = false)
b
b
b
A[[l1 ]](m)
b ≺ A[[l2 ]](m)
b
b m)
b n
A[[l]](
b ≺
b 1 ]](m)
b 2 ]](m)
b B[[b
B[[b
b ∧
b
b 1 ]](m)
b 2 ]](m)
b B[[b
B[[b
b ∨
b
b
¬
b B[[b]](
m)
b
⊤

m[x
b 7→ ([−∞, +∞], βx )]
m[x
b 7→ ([−∞, +∞], ⊤)]
b
m[x
b 7→ A[[a]](
m)]
b
b
m[x
b 7→ A[[a]](
m)
b ⊔ m(x)]
b
m
b
b 2 ]] ◦ C[[c
b 1 ]])(m)
(C[[c
b
b
b 1 ]], C[[c
b 2 ]])(m)
[
cond(B[[b]], C[[c
b
b
b
(fix F )(m)
b
b
b
[ B[[b]],
cond(
g ◦ C[[c]],
λx.x)

([−∞, +∞], βx ) x ∈ Xi
([−∞, +∞], ⊤) x ∈ Xa

Figure 5: Abstract semantics
infinite interval domain, in order to guarantee the termination of the analysis. We use the standard widening operator
b and cond
d in
in [Cousot and Cousot, 1977]. The function fix
Figure 5 denote a post-fixed point operator and a sound abstraction of cond, respectively.
Pruning Next we describe how we do pruning with the static
analysis. Suppose we are given examples E ⊆ V × V and
a state s with input (x) and output (y) variables. For each
example (vi , vo ) ∈ E, we first run the static analysis with the
input α(vi ) and obtain the analysis result (itvs , se s ) :
b
(itvs , se s ) = (C[[s]]([x
7→ α(vi )])(y).

We only consider the case when itvs = [ls , us ] (when itvs =
⊥, the program is semantically ill-formed and therefore we
just prune out the state). Then, we obtain the interval abstraction [lo , uo ] of the output vo , i.e., ([lo , uo ], −) = α(vo ), and
s
generate the constraints C(v
:
i ,vo )
s
C(v
= (ls ≤ lo ∧ uo ≤ us ) ∧ (se ∈ SE =⇒ lo ≤ se ≤ uo ).
i ,vo )

The first (resp., second) conjunct means that the interval
(resp., symbolic) analysis result must over-approximate the
s
output example. We prune out a state s iff C(v
is unsatisi ,vo )
fiable for some example (vi , vo ) ∈ E:
Definition 2. The predicate prune is defined as follows:
s
prune(s) ⇐⇒ C(v
is unsatisfiable for some (vi , vo ) ∈ E.
i ,vo )

The unsatisfiability can be easily checked, for instance,
with an off-the-shelf SMT solver. Our pruning is safe:

Theorem 1 (Safety). ∀s ∈ S. prune(s) =⇒ fail(s).
That is, we prune out a state only when it is a failure state,
which formally guarantees that the search algorithm with our
pruning finds a solution if and only if the baseline algorithm
(Section 4.2) does so.

5 Evaluation
Experimental setup To evaluate our synthesis algorithm, we
gathered 30 introductory level problems from several online
forums (Table 1).2 The problems consist of tasks manipulating integers and arrays. Some problems are non-trivial for
novice students to solve; they require students to come up
with various control structures such as nested loops and combinations of loops and conditional statements. The partial
programs we used are similar to those shown in Section 2;
they have one boolean expression hole (△), and one or two
command holes (). For each benchmark, we report the
number of integer variables (IVars), array variables (AVars),
integer constants (Ints), and examples (Exs) provided, respectively. All benchmark problems are publicly available with
our tool. Experiments were conducted on MacBook Pro with
Intel Core i7 and 16GB of memory.
Baseline Algorithm Table 1 shows the performance of our
algorithm. The column “Base” shows the running time of our
baseline algorithm that performs enumerative search without
state normalization. In that case, the average runtime was
longer than 616 seconds, and three of the benchmarks timed
out (> 1 hour). The column “Base+Opt” reports the performance of the baseline with normalization. It shows that
normalizing states succeeds to solve all benchmark problems
and improves the speed by more than 3.7 times on average,
although it degrades the speed for some cases due to runtime
normalization overhead.
Pruning Effectiveness On top of “Base+Opt”, we applied
our static-analysis-guided pruning technique (the column
“Ours”). The results show that our pruning technique is remarkably effective. It reduces the average time to 6.6 seconds, improving the speed of “Base+Opt” by 25 times. Note
that S IMPL is able to synthesize the desired programs from a
few examples (Exs), requiring up to 4 examples.

6 Related Work
Computer-aided education Recently, program synthesis
technology has revolutionized computer-aided education.
For instance, the technology has been used in automatic
problem generation [Singh et al., 2012; Ahmed et al., 2013;
Alvin et al., 2014; Polozov et al., 2015], automatic grading [Alur et al., 2013], and automatic solution generation [Gulwani et al., 2011].
Our work is to use program synthesis for automated
programming education system.
A large amount of
work has been done to automate programming education [Adam and Laurent, 1980; Soloway et al., 1981;
Farrell et al., 1984;
Johnson and Soloway, 1984;
Murray, 1989; Singh et al., 2013; Gulwani et al., 2014;
Kaleeswaran et al., 2016; Kim et al., 2016], which focuses
2

E.g., http://www.codeforwin.in

Domain

Integer

Array

Vars

No

Description

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

Given n, return n!.
Given n, return n!! (i.e., double factorial).
P
Given n, return ni=1 i.
P
Given n, return ni=1 i2 .
Q
Given n, return ni=1 i2 .
Given a and n, return an .
P
Given n and m, return m
i.
Q i=n
Given n and m, return m
i=n i.
Count the number of digit for an integer.
Sum the digits of an integer.
Calculate product of digits of an intger.
Count the number of binary digit of an integer.
Find the nth Fibonacci number.
P
P
Given n, return ni=1 ( im=1 m)).
Qn Qi
Given n, return i=1 ( m=1 m)).
Reverse a given integer.
Find the sum of all elements of an array.
Find the product of all elements of an array.
Sum two arrays of same length into one array.
Multiply two arrays of same length into one array.
Cube each element of an array.
Manipulate each element into 4th power.
Find a maximum element.
Find a minimum element.
Add 1 to each element.
Find the sum of square of each element.
Find the multiplication of square of each element.
Sum the products of matching elements of two arrays.
Sum the absolute values of each element.
Count the number of each element.
Average

IVars

AVars

2
3
3
4
4
4
3
3
3
3
3
2
3
3
3
3
3
3
3
3
3
3
3
3
2
3
3
3
2
3

0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
1
1
2
2
1
1
1
1
1
1
1
2
1
1

Ints

Exs

2
3
2
2
2
2
2
2
3
3
3
3
3
2
2
3
2
2
2
2
1
1
2
2
1
2
1
1
1
3

4
4
4
3
3
4
3
3
3
4
3
3
4
4
4
3
2
2
2
2
2
2
2
2
3
2
2
3
2
2

Base
0.0
0.0
0.1
122.4
102.9
0.7
0.2
0.2
0.0
5.2
0.7
0.0
98.7
⊥
⊥
⊥
8.1
7.6
44.6
47.4
1283.3
1265.8
0.9
0.8
0.3
2700.0
1709.8
20.5
45.0
238.9
> 616.8

Time (sec)
Base+Opt
0.0
0.0
0.0
18.1
13.6
0.1
0.0
0.0
0.0
2.2
2.3
0.0
13.9
324.9
316.6
367.3
3.6
3.9
29.9
26.4
716.1
715.5
0.7
0.3
0.0
186.2
1040.3
38.7
50.5
1094.1
165.5

Ours
0.0
0.0
0.0
0.3
0.2
0.1
0.0
0.1
0.0
1.3
0.3
0.0
2.6
37.6
86.9
2.5
0.9
0.9
0.2
0.3
13.0
13.0
0.4
0.1
0.0
11.5
12.6
1.5
12.1
0.2
6.6

Table 1: Performance of S IMPL . ⊥ denotes timeout (> 1 hour). Assume ⊥ as 3,600 seconds for the average of “Base”.
primarily on providing feedback on students’ programming submissions. Our system, S IMPL , has the following
advantages over prior works:
• Feedback on incomplete programs: Existing systems
produce feedback only for complete programs; they cannot help students who do not know how to proceed further. In this case, S IMPL can help by automatically generating solutions starting from incomplete solutions.
• No burden on instructor: Existing systems require
instructor’s manual effort. For example, the system
in [Singh et al., 2013] needs a correct implementation
and a set of correction rules manually designed by the
instructor. On the other hand, S IMPL does not require
anything from the instructor.
An exception is [Farrell et al., 1984], where an automatic LISP feedback system is presented. However, the
system produces feedback by relying on ad-hoc rules.
Programming by example Our work differs from
prior programming-by-example (PBE) techniques in
two ways. First, to our knowledge, our work is the
first to synthesize imperative programs with loops.
Most of the PBE approaches focus on domain-specific

languages for string transformation [Gulwani, 2011;
Kini and Gulwani, 2015;
Raza et al., 2015;
Manshadi et al., 2013; Wu and Knoblock, 2015],
number transformation [Singh and Gulwani, 2012], XML
transformation [Raza et al., 2014], and extracting relational data [Le and Gulwani, 2014], etc.
Several
others have studied synthesis of functional programs
[Albarghouthi et al., 2013;
Osera and Zdancewic, 2015;
Frankle et al., 2016]. Second, our algorithm differs from
prior work in that we combine semantic-based static analysis
technology with enumerative program synthesis. Existing
enumerative synthesis technology used pruning techniques such as type systems [Osera and Zdancewic, 2015;
Frankle et al., 2016] and deductions [Feser et al., 2015],
which are not applicable to our setting.

7 Conclusion
In this paper, we have shown that combining enumerative
synthesis and static analysis is a promising way of synthesizing introductory imperative programs. The enumerative
search allows us to find the smallest possible, therefore general, program while the semantics-based static analysis dra-

matically accelerates the process in a safe way. We demonstrated the effectiveness on 30 real programming problems
gathered from online forums.

References
[Adam and Laurent, 1980] Anne Adam and Jean-Pierre Laurent. Laura, a system to debug student programs. Artificial
Intelligence, 15(1-2), November 1980.
[Ahmed et al., 2013] Umair Z. Ahmed, Sumit Gulwani, and
Amey Karkare. Automatically generating problems and
solutions for natural deduction. In IJCAI, 2013.
[Aho et al., 1986] Alfred V. Aho, Ravi Sethi, and Jeffrey D.
Ullman. Compilers: Principles, Techniques, and Tools.
Addison-Wesley Longman Publishing Co., Inc., Boston,
MA, USA, 1986.
[Albarghouthi et al., 2013] Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. Recursive program synthesis.
In CAV, 2013.
[Alur et al., 2013] Rajeev Alur, Loris D’Antoni, Sumit Gulwani, Dileep Kini, and Mahesh Viswanathan. Automated
grading of dfa constructions. In IJCAI, 2013.
[Alvin et al., 2014] Chris Alvin, Sumit Gulwani, Rupak Majumdar, and Supratik Mukhopadhyay. Synthesis of geometry proof problems. In AAAI, 2014.
[Cousot and Cousot, 1977] Patrick Cousot and Radhia
Cousot.
Abstract interpretation: A unified lattice
model for static analysis of programs by construction or
approximation of fixpoints. In POPL, 1977.
[Farrell et al., 1984] Robert G. Farrell, John R. Anderson,
and Brian J. Reiser. An interactive computer-based tutor
for lisp. In AAAI, 1984.
[Feser et al., 2015] John K. Feser, Swarat Chaudhuri, and
Isil Dillig. Synthesizing data structure transformations
from input-output examples. In PLDI, 2015.
[Frankle et al., 2016] Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Exampledirected synthesis: A type-theoretic interpretation. In
POPL, 2016.
[Gulwani et al., 2011] Sumit Gulwani, Vijay Anand Korthikanti, and Ashish Tiwari. Synthesizing geometry constructions. In PLDI, 2011.
[Gulwani et al., 2014] Sumit Gulwani, Ivan Radiček, and
Florian Zuleger. Feedback generation for performance
problems in introductory programming assignments. In
FSE, 2014.
[Gulwani, 2011] Sumit Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL,
2011.
[Johnson and Soloway, 1984] W. Lewis Johnson and Elliot
Soloway. Proust: Knowledge-based program understanding. In ICSE, 1984.
[Kaleeswaran et al., 2016] Shalini Kaleeswaran, Anirudh
Santhiar, Aditya Kanade, and Sumit Gulwani. Semisupervised verified feedback generation. In FSE, 2016.

[Kim et al., 2016] Dohyeong Kim, Yonghwi Kwon, Peng
Liu, I. Luk Kim, David Mitchel Perry, Xiangyu Zhang, and
Gustavo Rodriguez-Rivera. Apex: Automatic programming assignment error explanation. In OOPSLA, 2016.
[Kini and Gulwani, 2015] Dileep Kini and Sumit Gulwani.
Flashnormalize: Programming by examples for text normalization. In IJCAI, 2015.
[Le and Gulwani, 2014] Vu Le and Sumit Gulwani. Flashextract: A framework for data extraction by examples. In
PLDI, 2014.
[Manshadi et al., 2013] Mehdi Manshadi, Daniel Gildea,
and James Allen. Integrating programming by example
and natural language programming. In AAAI, 2013.
[Murray, 1989] William R. Murray. Automatic Program DeBugging for Intelligent Tutoring Systems. Morgan Kaufmann Publishers Inc., 1989.
[Osera and Zdancewic, 2015] Peter-Michael Osera and
Steve Zdancewic. Type-and-example-directed program
synthesis. In PLDI, 2015.
[Polozov et al., 2015] Oleksandr
Polozov,
Eleanor
O’Rourke, Adam M. Smith, Luke Zettlemoyer, Sumit
Gulwani, and Zoran Popovic. Personalized mathematical
word problem generation. In IJCAI, 2015.
[Raza et al., 2014] Mohammad Raza, Sumit Gulwani, and
Natasa Milic-Frayling. Programming by example using
least general generalizations. In AAAI, 2014.
[Raza et al., 2015] Mohammad Raza, Sumit Gulwani, and
Natasa Milic-Frayling. Compositional program synthesis
from natural language and examples. In IJCAI, 2015.
[Singh and Gulwani, 2012] Rishabh Singh and Sumit Gulwani. Synthesizing number transformations from inputoutput examples. In CAV, 2012.
[Singh et al., 2012] Rohit Singh, Sumit Gulwani, and Sriram
Rajamani. Automatically generating algebra problems. In
AAAI, 2012.
[Singh et al., 2013] Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama. Automated feedback generation for
introductory programming assignments. In PLDI, 2013.
[Soloway et al., 1981] Elliot M. Soloway, Beverly Woolf,
Eric Rubin, and Paul Barth. Meno-ii: An intelligent tutoring system for novice programmers. In IJCAI. Morgan
Kaufmann Publishers Inc., 1981.
[Wu and Knoblock, 2015] Bo Wu and Craig A. Knoblock.
An iterative approach to synthesize data transformation
programs. In IJCAI, 2015.

