@inproceedings{HJK10,
title = {Synthesis for regular specifications over unbounded domains },
author = {Hamza, Jad and Jobstmann, Barbara and Kuncak, Viktor},
year = {2010},
booktitle = {Conference on Formal Methods in Computer Aided Design, FMCAD 2010, Lugano, CH},
team = {DCS},
abstract = {Synthesis from declarative specifications is an ambitious
automated method for obtaining systems that are correct by construction.
Previous work includes synthesis of reactive finite-state
systems from linear temporal logic and its fragments.
Further recent work focuses on a different application area
by doing functional synthesis over unbounded domains, using
a modified Presburger arithmetic quantifier elimination
algorithm. We present new algorithms for functional
synthesis over unbounded domains based on automata-theoretic
methods, with advantages in the expressive power and in the
efficiency of synthesized code.
Our approach synthesizes functions that meet given regular
specifications defined over unbounded sequences of input and
output bits. Thanks to the translation from weak monadic
second-order logic to automata, this approach supports full
Presburger arithmetic as well as bitwise operations on
arbitrary length integers. The presence of quantifiers
enables finding solutions that optimize a given criterion.
Unlike synthesis of reactive systems, our notion of
realizability allows functions that require examining the
entire input to compute the output. Regardless of the
complexity of the specification, our algorithm synthesizes
linear-time functions that read the input and directly
produce the output. We also describe a technique to
synthesize functions with bounded lookahead when possible,
which is appropriate for streaming implementations. We
implemented our synthesis algorithm and show that it
synthesizes efficient functions on a number of examples.
},
}
