PLClub Discussion Group

Provenance-Guided Synthesis of Datalog Programs

I will speak this Friday at PL club about this paper (https://www.cis.upenn.edu/~mhnaik/papers/popl20.pdf), “Provenance-Guided Synthesis of Datalog Programs,” which I read recently for an independent study. This paper gives a approach for synthesizing a Datalog program from input-output examples. The approach uses a Datalog solver to determine why a candidate program produces an undesired output (“why” provenance), and its key insight is that we can determine why a candidate program fails to produce a desired output (“why not” provenance). My goal for this talk is to improve my understanding of the paper.

Homework:

1. look at some examples of Datalog syntax https://en.wikipedia.org/wiki/Datalog

2. learn about counterexample-guided inductive synthesis, the paradigm this paper uses for synthesis; section 2.2 of this paper https://www.kroening.com/papers/cav2018-synthesis.pdf gives an overview