Skip to main content

Lazy but Effective Functional Synthesis

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

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorFedyukovich, Grigory-
dc.contributor.authorGurfinkel, Arie-
dc.contributor.authorGupta, Aarti-
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.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.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

Files in This Item:
File Description SizeFormat 
EffectiveFunc.pdf544.25 kBAdobe PDFView/Download

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.