Program Extrapolation with Jennisys

The desired behavior of a program can be described using an abstract

model. Compiling such a model into executable code requires advanced

compilation techniques known as synthesis. This paper presents a

language, called Jennisys, where programming is done by introducing an

abstract model, defining a concrete data representation for the model,

and then being aided by automatic synthesis to produce executable

code. The paper also presents a synthesis technique for the language.

The technique is built on an automatic program verifier that, via an

underlying SMT solver, is capable of providing concrete models

to failed verifications. The technique proceeds by obtaining sample

input/output values from concrete models and then extrapolating programs from

the sample points. The synthesis aims to produce code with

assignments, branching structure, and possibly recursive calls.

A prototype of the language and synthesis technique has been

implemented.

krml219.pdf
PDF file

Publisher  Microsoft Technical Report

Details

TypeTechReport
NumberMSR-TR-2012-12
> Publications > Program Extrapolation with Jennisys