Hi everyone,
Today I'll be presenting the paper Synthesizing
Imperative Programs for Introductory Programming Assignments (ISAS 2017) [link].
This paper presents a tool, SIMPL,
for synthesizing imperative programs given a partial program and a set of input-output examples. SIMPL performs
top-down enumerative search, incorporating a novel static analysis step to prune partial programs that cannot satisfy the constraints.
As usual, we'll be getting started at 1pm CET on Zoom [link].
"Homework question": one of the static analysis checks performed by SIMPL uses
the abstract interval domain to test whether each example's output values are within a range of integers that could be produced by the program. Can you think of a way to extend this analysis to support constraints with universally quantified variables, e.g. max(x,
x+1) = x+1?
Best,
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}