Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 14:30 - 15:00 at Sala III - Program Synthesis Chair(s): Nuno P. Lopes

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 Jan

14:00 - 15:30: VMCAI 2019 - Program Synthesis at Sala III
Chair(s): Nuno P. LopesMicrosoft Research
VMCAI-201914:00 - 14:30
Jad HamzaLIAFA, Université Paris Diderot, Viktor KunčakEPFL, Switzerland
VMCAI-201914:30 - 15:00
Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University
VMCAI-201915:00 - 15:30
Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore