Lazy but Effective Functional Synthesis
We present a new technique for generating a function implementation from a declarative specification formulated as a Forall-Exists-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.
Sun 13 JanDisplayed time zone: Belfast change
14:00 - 15:30
|Minimal Synthesis of String To String Functions From Examples|
|Lazy but Effective Functional Synthesis|
|Automatic Program Repair using Formal Verification and Expression Templates|