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

We study the problem of synthesizing string to string transformations from a set of input/output examples. The transformations we consider are expressed using deterministic finite automata (DFA) that read pairs of letters, one letter from the input and one from the output. The DFA corresponding to these transformations have additional constraints, ensuring that each input string is mapped to exactly one output string.

We suggest that, given a set of input/output examples, the smallest DFA consistent with the examples is a good candidate for the transformation the user was expecting. We therefore study the problem of, given a set of examples, finding a minimal DFA consistent with the examples and satisfying the functionality and totality constraints mentioned above.

We prove that, in general, this problem (the corresponding decision problem) is NP-complete. This is unlike the standard DFA minimization problem which can be solved in polynomial time. We provide several NP-hardness proofs that show the hardness of multiple (independent) variants of the problem.

Finally, we propose an algorithm for finding the minimal DFA consistent with input/output examples, that uses a reduction to SMT solvers. We implemented the algorithm, and used it to evaluate the likelihood that the minimal DFA indeed corresponds to the DFA expected by the user.

Sun 13 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. Lopes Microsoft Research
14:00
30m
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad Hamza LIAFA, Université Paris Diderot, Viktor Kunčak EPFL, Switzerland
14:30
30m
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University
15:00
30m
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen , Quang-Trung Ta National University of Singapore, Wei-Ngan Chin National University of Singapore