Comfusy: Complete Functional Synthesis (Tool Presentation)

paper ps   
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy symbolically computes the precise domain for the given relation and generates the function from inputs to outputs. The outputs are guaranteed to satisfy the relation whenever the inputs belong to the relation domain. The core of our synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables. We present examples that demonstrate software synthesis using Comfusy, and illustrate how synthesis simplifies software development.

Citation

Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter. Comfusy: Complete functional synthesis (tool presentation). In CAV, 2010.

BibTex Entry

@inproceedings{KuncakETAL10Comfusy,
  author = {Viktor Kuncak and Mikael Mayer and Ruzica Piskac and Philippe Suter},
  title = {Comfusy: Complete Functional Synthesis (Tool Presentation)},
  booktitle = {CAV},
  abstract = {Synthesis of program fragments from specifications can make
programs easier to write and easier to reason about. We
present Comfusy, a tool that extends the compiler for the
general-purpose programming language Scala with
(non-reactive) functional synthesis over unbounded
domains. Comfusy accepts expressions with input and output
variables specifying relations on integers and sets.
Comfusy symbolically computes the precise domain for the
given relation and generates the function from inputs to
outputs. The outputs are guaranteed to satisfy the relation
whenever the inputs belong to the relation domain. The core
of our synthesis algorithm is an extension of quantifier
elimination that generates programs to compute witnesses for
eliminated variables. We present examples that demonstrate
software synthesis using Comfusy, and illustrate how
synthesis simplifies software development.},
  year = 2010
}