# Lazy but Effective Functional Synthesis

## Author(s): Fedyukovich, Grigory; Gurfinkel, Arie; Gupta, Aarti

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1zk2n
DC FieldValueLanguage
dc.contributor.authorFedyukovich, Grigory-
dc.contributor.authorGurfinkel, Arie-
dc.contributor.authorGupta, Aarti-
dc.date.accessioned2021-10-08T19:50:27Z-
dc.date.available2021-10-08T19:50:27Z-
dc.date.issued2019en_US
dc.identifier.citationFedyukovich, Grigory, Arie Gurfinkel, and Aarti Gupta. "Lazy but Effective Functional Synthesis." In International Conference on Verification, Model Checking, and Abstract Interpretation (2019): pp. 92-113. doi:10.1007/978-3-030-11245-5_5en_US
dc.identifier.issn0302-9743-
dc.identifier.urihttps://www.cs.fsu.edu/~grigory/aeval.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1zk2n-
dc.description.abstractWe present a new technique for generating a function implementation from a declarative specification formulated as a ∀∃ -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.en_US
dc.format.extent92 - 113en_US
dc.language.isoen_USen_US
dc.relation.ispartofInternational Conference on Verification, Model Checking, and Abstract Interpretationen_US
dc.rightsAuthor's manuscripten_US
dc.titleLazy but Effective Functional Synthesisen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1007/978-3-030-11245-5_5-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat