TY - GEN
T1 - Lazy but effective functional synthesis
AU - Fedyukovich, Grigory
AU - Gurfinkel, Arie
AU - Gupta, Aarti
N1 - Funding Information:
This work was supported in part by NSF Grant 1525936. Any opinions, findings, and conclusions expressed herein are those of the authors and do not necessarily reflect those of the NSF.
Funding Information:
We thank Andreas Katis for providing encodings of benchmarks for reactive synthesis from Assume-Guarantee contracts into an SMT-LIB2 format acceptable by AE-VAL. This work was supported in part by NSF Grant 1525936. Any opinions, findings, and conclusions expressed herein are those of the authors and do not necessarily reflect those of the NSF.
PY - 2019
Y1 - 2019
N2 - We present a new technique for generating a function implementation from a declarative specification formulated as a (Formula presented)-formula in first-order logic. We follow a classic approach of eliminating existential quantifiers and extracting Skolem functions for the theory of linear arithmetic. Our method eliminates quantifiers lazily and produces a synthesis solution in the form of a decision tree. Compared to prior approaches, our decision trees have fewer nodes due to deriving theory terms that can be shared both within a single output as well as across multiple outputs. Our approach is implemented in a tool called AE-VAL, and its evaluation on a set of reactive synthesis benchmarks shows promise.
AB - We present a new technique for generating a function implementation from a declarative specification formulated as a (Formula presented)-formula in first-order logic. We follow a classic approach of eliminating existential quantifiers and extracting Skolem functions for the theory of linear arithmetic. Our method eliminates quantifiers lazily and produces a synthesis solution in the form of a decision tree. Compared to prior approaches, our decision trees have fewer nodes due to deriving theory terms that can be shared both within a single output as well as across multiple outputs. Our approach is implemented in a tool called AE-VAL, and its evaluation on a set of reactive synthesis benchmarks shows promise.
UR - http://www.scopus.com/inward/record.url?scp=85061107525&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85061107525&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-11245-5_5
DO - 10.1007/978-3-030-11245-5_5
M3 - Conference contribution
AN - SCOPUS:85061107525
SN - 9783030112448
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 92
EP - 113
BT - Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
A2 - Piskac, Ruzica
A2 - Enea, Constantin
PB - Springer Verlag
T2 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2019
Y2 - 13 January 2019 through 15 January 2019
ER -