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.

Conference Day
Sun 13 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. LopesMicrosoft Research
14:00
30m
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad HamzaLIAFA, Université Paris Diderot, Viktor KunčakEPFL, Switzerland
14:30
30m
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University
15:00
30m
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore