K. Rustan M. Leino and Aleksandar Milicevic
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
Publisher Microsoft Technical Report