Program Synthesis for Hierarchical Specifications

Thibaud Hottelier and Ras Bodik

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2014-139
July 29, 2014

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-139.pdf

Synthesis is the problem of obtaining programs from relational specifications. We present grammar-modular (GM) synthesis, an algorithm for synthesis from tree-structured relational specifications. GM synthesis makes synthesis applicable to previously intractable relational specifications by decomposing them into smaller subproblems, which can be tackled in isolation by off-the-shelf synthesis procedures. The program fragments thus generated are subsequently composed to form a program satisfying the overall specification.

We also generalize our technique to tree languages of relational specifications. Here, we synthesize a single program capable satisfying any (tree-shaped) relation belonging to the language; the synthesized program is syntax-directed by the structure of the relation.

We evaluate our work by applying GM synthesis to document layout: given the semantics of a layout language, we synthesize tailored constraint solvers capable of laying out languages of documents. Our experiments show that GM synthesis is sufficiently complete to successfully generate solvers for non-trivial data visualizations, and that our synthesized solvers are between 39- to 200-times faster than general-purpose constraint solvers.


BibTeX citation:

@techreport{Hottelier:EECS-2014-139,
    Author = {Hottelier, Thibaud and Bodik, Ras},
    Title = {Program Synthesis for Hierarchical Specifications},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2014},
    Month = {Jul},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-139.html},
    Number = {UCB/EECS-2014-139},
    Abstract = {Synthesis is the problem of obtaining programs from relational specifications. We present grammar-modular (GM) synthesis, an algorithm for synthesis from tree-structured relational specifications. GM synthesis makes synthesis applicable to previously intractable relational specifications by decomposing them into smaller subproblems, which can be tackled in isolation by off-the-shelf synthesis procedures. The program fragments thus generated are subsequently composed to form a program satisfying the overall specification.

We also generalize our technique to tree languages of relational specifications. Here, we synthesize a single program capable satisfying any (tree-shaped) relation belonging to the language; the synthesized program is syntax-directed by the structure of the relation. 

We evaluate our work by applying GM synthesis to document layout: given the semantics of a layout language, we synthesize tailored constraint solvers capable of laying out languages of documents. Our experiments show that GM synthesis is sufficiently complete to successfully generate solvers for non-trivial data visualizations, and that our synthesized solvers are between 39- to 200-times faster than general-purpose constraint solvers.}
}

EndNote citation:

%0 Report
%A Hottelier, Thibaud
%A Bodik, Ras
%T Program Synthesis for Hierarchical Specifications
%I EECS Department, University of California, Berkeley
%D 2014
%8 July 29
%@ UCB/EECS-2014-139
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-139.html
%F Hottelier:EECS-2014-139