@techreport{gulwani2009component,
author = {Gulwani, Sumit and Venkatesan, Ramarathnam},
title = {Component Based Synthesis Applied to Bitvector Circuits},
year = {2009},
month = {April},
abstract = {We define "component-based synthesis" to be the problem of synthesis 
of (straight-line) programs from appropriate composition of base components 
from a specified library of software components. The functional
specification of the desired program and the library components is
provided in the form of logical formulas that relate the respective input and
output variables. This has applications in design of intricate
circuits or algorithms, superoptimization, and API mining. Furthermore,
automated synthesis provides the promise of correctness by construction, 
generation of efficient systems, and improvement in developer's productivity.
We solve the component-based synthesis problem using a constraint-based
approach that involves first generating a "synthesis constraint",
and then solving the constraint. The synthesis constraint is a first-order 
logic formula whose size is quadratic in the number of components, 
but has quantifier alternation. We present a novel algorithm for 
solving such constraints. Our algorithm is based on counterexample 
guided iterative synthesis paradigm and uses off-the-shelf SMT solvers. 
We present experimental results on synthesizing a variety of bitvector
algorithms that involve unintuitive composition of
standard bitvector operations and are difficult to synthesize
manually. We also compare our technique with existing synthesis
approaches based on sketching and superoptimization.
Our tool Brahma can efficiently synthesize highly nontrivial
10-20 line loop-free programs. These programs 
represent a state space of approximately 2010 programs, and 
are beyond the reach of the other tools.},
publisher = {Microsoft Research},
url = {http://approjects.co.za/?big=en-us/research/publication/component-based-synthesis-applied-to-bitvector-circuits/},
number = {MSR-TR-2010-12},
}