Functional Synthesis with Examples

Speaker:
Grigory Fedyukovich, Florida State University, USA

Abstract:
Functional synthesis (FS) aims at generating a program from its declarative specification over sets of designated input and output variables. Traditionally, FS tasks are formulated as \forall\exists-formulas, where input variables are universally quantified and output variables are existentially quantified. State-of-the-art approaches to FS proceed by eliminating existential quantifiers and extracting Skolem functions, which are then turned into implementations. Related applications benefit from having concise (i.e., compact and comprehensive) Skolem functions. In this talk, I will present a technique for generating Skolem functions in linear arithmetic that eliminates existential quantifiers lazily and produces a synthesis solution in the form of a decision tree. I will also present an approach for extracting concise Skolem functions for FS tasks specified as examples, i.e., tuples of concrete values of variables. The decision tree is built from relationships between inputs and outputs and preconditions that classify all examples into subsets that share the same input-output relationship. The approaches are implemented in a tool called AE-VAL, and its evaluation on a set of reactive synthesis benchmarks shows promise.

Biography:
Dr. Grigory Fedyukovich is an Assistant Professor at Florida State University, USA. He completed his Ph.D. at the University of Lugano, Switzerland, under the supervision of Prof Natasha Sharygina, and then he was a postdoc at the University of Washington with Prof Rastislav Bodik and at Princeton University with Prof Aarti Gupta. His research interests are in software verification and synthesis, program equivalence, and applications of relational verification to analyzing software security.

Host: Prof. Natasha Sharygina