To refer to this page use:
|Abstract:||We 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.|
|Citation:||Fedyukovich, 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_5|
|Pages:||92 - 113|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Conference on Verification, Model Checking, and Abstract Interpretation|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.