Program Extrapolation with Jennisys

K. Rustan M. Leino and Aleksandar Milicevic

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2012-12
PublisherMicrosoft Technical Report
> Publications > Program Extrapolation with Jennisys