Skip to main content

Lazy but Effective Functional Synthesis

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

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.
Publication Date: 2019
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
DOI: 10.1007/978-3-030-11245-5_5
ISSN: 0302-9743
Pages: 92 - 113
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Verification, Model Checking, and Abstract Interpretation
Version: Author's manuscript

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